Predicate Abstraction is a method of synthesizing the strongest inductive invariant of a system expressible as a boolean combination of a set of atomic predicates. A predicate selection method can be said to be complete for a theory if it is eventually guaranteed to find the set of atomic predicates sufficient to prove a given property, when such exist. Current heuristics are incomplete and often diverge on simple examples. We present a practical method of predicate selection that is complete in the above sense. The method is based on interpolation and uses a "split-prover", somewhat in the style of structure-based provers used in Artificial Intelligence. We show that it allows the verification of a variety of simple programs that cannot be verified by existing software model checkers.
Proceedings of the 12th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2006