Abstract

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.