Ken McMillan (Cadence), Consequence Generation, Interpolants and Invariant Discovery

Most abstraction techniques can be viewed as language restrictions. Typically, given a restricted language L, we attempt to construct the strongest inductive invariant of a program expressible in L. In predicate abstraction, for example, L is the language of quantifier-free first order formulas over the program variables, with some given interpreted symbols. An abstraction refinement heuristic can be thought of as generating an increasing sequence of sub-languages of L, in the hope that one of these will contain an inductive invariant that proves a given property. For example, in predicate abstraction, each sub-language is restricted to use only a given finite set of atomic predicates. Such a heuristic might be said to be complete (relative to L) if it is guaranteed to eventually produce a sub-language of L proving a given property, when one exists.

Unfortunately, the abstraction heuristics the we currently use for infinite-state systems are generally incomplete. They can diverge, generating an infinite sequence of abstractions, even on trivial programs. Most of the counterexample-based heuristics can be viewed as refining the abstraction sub-language by supplementing it with the language used in the refutation of a counterexample. We will see that this approach can be made complete by restricting the language of these refutations. In effect, we divide the prover that refutes counterexamples into a sequence of provers, each of which knows only one step of the counterexample. By restricting the language in which these provers communicate, we can control the language of the resulting refinement (in fact, we can generate in interpolant in the restricted language, if one exists). Then by gradually relaxing this restriction, we can guarantee to eventually find an inductive invariant if one exists in L, and thus obtain a complete refinement heuristic. As we will observe, this approach is efficient enough to be used in the verification of large programs using predicate abstraction.