Constraint-Based Invariant Inference overPredicate Abstraction

摘要

This paper describes a constraint-based invariant generationtechnique for proving the validity of safety assertions over the domain ofpredicate abstraction in an interprocedural setting. The key idea of thetechnique is to represent each invariant in bounded DNF form by meansof boolean indicator variables, one for each predicate p and each disjunctd denoting whether p is present in d or not. The verification condition ofthe program is then encoded by means of a boolean formula over theseboolean indicator variables such that any satisfying assignment to theformula yields the inductive invariants for proving the validity of givenprogram assertions. This paper also describes how to use the constraint-based methodol-ogy for generating maximally-weak preconditions for safety assertions.An interesting application of maximally-weak precondition generationis to produce maximally-general counterexamples for safety assertions.We also present preliminary experimental evidence demonstrating thefeasibility of this technique.