Printable Version of this PageHome PageRecent ChangesSearchSign In

Program Verification Techniques II

Hoare-Flyod-Dijkstra's "Inductive Invariant" technique is the right way of using induction for proving properties of imperative programs.

For functional programs, induction works very well to prove program properties. The type of induction that is used for this is called "well founded induction". It is based on the observation that the argument passed in each recursive call becomes "smaller" – imagine a recursive function working on a list that passes the tail of the its argument to each recursive call.

But when we translate an imperative program with loop to a recursive functional program, the arguments to recursive calls do not become "smaller". So well-founded induction does not apply naturally to reasoning imperative program. I realized this from my ACL2 experiments. After reading some classic papers from seventies, I realized that Hoare's technique of "inductive invariants" was invented precisely for this purpose: to use induction for imperative programs. Although another inductive technique, called "subgoal induction", was proposed for imperative programs, Hoare-Flyod-Dijktra's inductive invariant technique has some nice properties and thus has become the classical technique for verification of imperative programs.

Limitation of inductive invariant technique is: it cannot produce a counterexample if the program is buggy.

There have been lots of work to infer loop invariants. Recent techniques proposed by Cormac Flanagan for ESC Java and Willem Visser for Java pathfinder to infer loop invariants are quite effective for real programs. But the major limitation of inductive invariant approach is, it cannot produce a counterexample if there is a bug in the program. If the program is buggy, either the technqiue will not be able to infer a loop invariant or the program does not verify from the infered invariant.

Advantage of model checking is: it can find a counter-example, which is why it has drawn the most attention in last five years.

A model checker can generate a counterexample because it exhaustively checks if the program property holds for each possible execution of the program. But on the other hand, its obvious limitation is, any useful program has infinite number of possible executions and thus it is impossible to check each of the infinite executions. But instead of being detered by this limitation, in last five years there have been increasing number of attempts to overcome this limitation. Besides bounded model checking, which unrolls the loop a fixed number of times, a sound solution to this problem is: Abstraction. From the program, derive an abstract program such that the abstract program has finite number of executions (so that each of them can be explored exhaustively) and if there is a bug in the original program then there must be a corresponding bug in the abstract program. But if the model checker finds a bug in the abstract program it does not necessarily indicate a bug in the original program. If such a situation occurs, the abstract program is "refined" (use more predicates for abstraction) to eliminate this spurious bug from the abstract program and the model checker is run again. This continues until either all executions have been explored and no bug is found in the abstract program or a bug in the abstract program corresponds to a real bug in the original program. This iterative process is called "Counterexample Guided Abstraction Refinement" (CEGAR). Predicate abstraction is the defacto abstraction technique that is used.

Effectiveness of predicate abstraction based model checking depends on the predicates chosen for the abstraction.

The input to a predicate abstraction tool is the program to be verified and a set of predicates. Output is an abstract program that has one boolean variable corresponding to each predicate and each of whose statements model the effect of statements of the original program on these predicates. The tradeoff is: if we increase the number of predicates number of possible executions increases and thus makes the model checking expensive. Whereas if number of predicates is less, there will be more spurious counterexamples and more refinements. So recently there have been a few papers on how to choose the "right" predicates.

Limitation of model checking is, verifying programs with heap objects and arrays is not straight-forward.

Much of the research on using model checking for verification has focused on checking control-based properties (eg. type-state properties). Using model checking for checking assertions involving data values (like the examples that inductive invariant technique can handle) is yet to be demonstrated. Willem Visser thinks it needs ingenuity.

What should I do?

  • Use inductive invariant technique, but try to produce a counterexample if the program is buggy.
  • Systematically use exhaustive testing for small size inputs using a Korat/JPF like tool for loop invariant inference. This maybe useful in producing a counterexample if the program is buggy.
  • Static and dynamic analysis for infering predicates that can be used for predicate abstraction. I have a nice name for this:) "Predicate Slicing".
  • Use model checking for proving assertions for programs with heap objects and arrays.
  • Read More!

Last modified 16 March 2005 at 11:41 pm by Saswat Anand