5 ms·
Coq is an interactive theorem-prover, which is exactly what it sounds like. You prove your theorems more or less by typing out the proofs and the system mechani
by wsxcde 12y ago
Coq is an interactive theorem-prover, which is exactly what it sounds like. You prove your theorems more or less by typing out the proofs and the system mechanically verifies that each step in your proof is sound. I've used Coq and I'll be honest. This is unquestionably a solid way to prove things about your program but it is too much of pain to expect this to have significant adoption in the "real" world.
In the hardware world, there's been a lot of progress in automated verification thanks to modern model checkers [1,2] (which incidentally build on modern SAT, and in some cases SMT, solvers [3-6]). The nice thing about model checkers is that you just specify the property you want proven and let the verifier crunch away and it will (hopefully) come up with a proof or a counterexample. This has been successful enough that there are companies like JASPER and OneSpin which make money by selling hardware companies formal verification tools.
I worked with JASPER's tools in the recent-ish past and one of the big things they seem to have done is make the tool much more usable. With the JASPER tool, it was much less of a pain to configure the model checker, abstract away parts of the design, keep track of the properties specified and proven, examine counter example traces and so forth than I was expecting. A lot of this sort of thing doesn't get done in academic tools like ABC because it doesn't count as research. But such improvements are extremely important if you want to push adoption of formal tools in an industrial setting. And from what I can see the emphasis on usability seems to paying off for JASPER.
Model checking in software has been less successful because the state explosion problem is much more pronounced but there have been notable success stories like Microsoft Research's SLAM project [7]. And I definitely think there is an opportunity here to build upon the algorithmic progress in automated verification in order to build tools that are much usable in a software setting.
[1] http://ecee.colorado.edu/~bradleya/ic3/ http://ecee.colorado.edu/~bradleya/ic3/
[2] http://www.eecs.berkeley.edu/~alanmi/abc/abc.htm http://www.eecs.berkeley.edu/~alanmi/abc/abc.htm
[3] https://www.princeton.edu/~chaff/zchaff.html https://www.princeton.edu/~chaff/zchaff.html
[4] http://minisat.se/ http://minisat.se/
[5] http://fmv.jku.at/picosat/ http://fmv.jku.at/picosat/
[6] http://z3.codeplex.com/ http://z3.codeplex.com/
[7] http://research.microsoft.com/en-us/projects/slam/ http://research.microsoft.com/en-us/projects/slam/
- rossjudson 12y agoI get what you're saying about the state explosion problem, but the article specifically calls out the idea of proving a lack of negative behaviors. It seems to me it might be quite useful to be able to prove, for example, that a program never reads memory at random, or that it never exceeds the bounds of any allocated buffer. That's a different problem scale than "prove the whole thing works as specified".
- gsnedders 12y agoSadly, it's not a different problem scale — the typical model is something similar to "for each state, does the property P hold?". Hence no matter the property (or complexity thereof), one must still enumerate all states.
- CHY872 12y agoOf course, one will attempt to also find equivalence classes for the states! The code long x = user_input(); if (x == 0) { violate_model(); } else { do_something(); } you would expect by any reasonable implementation to collapse the system into just two equivalent states that can be tested.
- wsxcde 12y agoAh, but finding equivalence classes of states is quite tricky! Obviously the naive approach of enumerating states and assigning them to equivalence classes is dead on arrival. You might be hinting at examining control flow predicates with your example. This technique is called predicate abstraction and underlies a lot of the SLAM effort. It works in certain scenarios - A statement which more or less captures the state of the field itself.
- CHY872 12y agoWhat I'm personally hinting at is symbolic/concolic execution. Essentially, each variable has a set of constraints associated with it - initially left blank for an input variable, for example. Then, the program can be executed, with assignments producing new constraints and replacing old ones. At each point in control flow, the executor chooses a path, and adds new constraints. When a dangerous statement (assertion, pointer dereference etc) is reached, the constraints can be solved by z3 or some other SMT solver, and if it can find a satisfying result you automatically have a test case that will produce erroneous or undefined behaviour. It works quite well for short programs, actually - the KLEE people (or maybe it was DART) found bugs in busybox, GNU Coreutils etc. The current approach is to instead of traversing your control flow tree explicitly (which means you're doing a tree search over a potentially infinite tree), converting the program such that it produces a logical statement that can be solved by an SMT solver, that is satisfiable iff there is an input that leads to a bug within that bounded number of loop unwindings. With fun C++ metaprogramming, you can actually get this to happen natively (i.e. the parts that aren't reliant on input get run natively) which leads to a massive speedup o I don't believe it to be model checking, although it might use model checking techniques. I could be wrong, I'm only familiar with a few aspects.