Program Verification using Templates over Predicate Abstraction
We address the problem of automatically generating invariants with quantified
and boolean structure for proving the validity of given assertions or
generating pre-conditions under which the assertions are valid. We present
three novel algorithms, having different strengths, that combine template and predicate
abstraction based formalisms to discover required sophisticated program
invariants using SMT solvers.
Two of these algorithms use an iterative approach to compute fixed-points (one
computes a least fixed-point and the other computes a greatest fixed-point),
while the third algorithm uses a constraint based approach to encode the
fixed-point. The key idea in all these algorithms is to reduce the problem of
invariant discovery to that of finding optimal solutions for unknowns
(over conjunctions of some predicates from a given set) in a template formula
such that the formula is valid.
Preliminary experiments using our implementation of these algorithms show
encouraging results over a benchmark of small but complicated programs. Our
algorithms can verify program properties that, to our knowledge, have not been
automatically verified before. In particular, our algorithms can generate full
correctness proofs for sorting algorithms (which requires nested
universally-existentially quantified invariants) and can also generate
preconditions required to establish worst-case upper bounds of sorting
algorithms. Furthermore, for the case of previously considered properties, in
particular sortedness in sorting algorithms, our algorithms take less time than
reported by previous techniques.