Download Verification Condition Splitting

If the elided code does not contain other return statements and does not update the local
variable t, then the postcondition follows directly, regardless of how many execution
paths go through the elided code. Patterns like these occur often enough in code that
it is worthwhile—and for ESC/Java, essential [10]—to structure the VC in a way that
allows the theorem prover to attempt the proof without having to do it once for each
execution path leading to the return statement.
Based on this insight, Boogie implemented an even more advanced encoding of
unstructured programs [4]. However, as evidence from numerous verification efforts
has shown, the resulting flat structure provides often too little guidance about a good
order in which to do case splits. And even lemma learning SAT solvers cannot always
overcome this problem. Our VC splitting technique reintroduces this program structure.
VC generators that use interactive or resolution-based theorem provers as backends, like the Why tool [8], usually split the VC completely (i.e., down to one path
and one assertion) before going to the prover. The Why tool even allows for further
splitting. This is understandable, as resolution is known not to handle case splits very
efficiently and for interactive provers reducing the size of the formula is essential for
the human being to understand it. However, because SMT solvers use rather different
search strategy than the resolution-based theorem provers, they are particularly good
at exploiting Boolean structure of the formula. It is only the interaction with quantifier
instantiation that sometimes causes them to fail: indeed both our experimental data and
[10] show that introducing too many splits slows down the verification process.
Our approach is therefore a middle ground between what Boogie used to do, thus
avoiding exponential explosion in the number of paths and what the Why tool does, thus
providing better error reporting, progress information and scalability in some cases.
Future Work It is likely that splitting inside the SMT solver would be more effective.
Let us call the CFG nodes, where the splitting algorithm would perform a split special.
Special CFG nodes correspond to special abstract syntax tree nodes in the VC. Special
nodes in the VC correspond to special Boolean literals in the CNF translation. For the
SMT solver splitting amounts to bumping activity of the special literals and cleaning
up the set of conflict clauses when backtracking through special literals. Implementing
such a strategy will require significant effort and unfortunately needs to be redone for
each SMT solver.
6
Conclusions
We have presented a method splitting verification conditions based on control flow. We
have proven the method correct and shown how it can be applied to bring enormous
speedups in some cases, compared to a monolithic VC. The method also bridges the
gap between the full VC splitting employed in some other verification systems and the
monolithic VC.
References
0. The HAVOC property checker, 2008.
projects/havoc/.
http://research.microsoft.com/
13