Constraint-based Invariant Inference over Predicate Abstraction

Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan

Abstract

This paper describes a constraint-based invariant generation technique for proving the validity of safety assertions over the domain of predicate abstraction in an interprocedural setting. The key idea of the technique is to represent each invariant in bounded DNF form by means of boolean indicator variables, one for each predicate pred and each disjunct disj denoting whether pred is present in disj or not. The verification condition of the program is then encoded by means of a boolean formula over these boolean indicator variables such that any satisfying assignment to the formula yields the inductive invariants for proving the validity of given program assertions. This paper also describes how to use the constraint-based methodology for generating maximally-weak preconditions for safety assertions. An interesting application of maximally-weak precondition generation is to produce maximally-general counterexamples for safety assertions. We also present preliminary experimental evidence demonstrating the feasibility of this technique.

Details

Publication typeTechReport
URLhttp://www.springer-ny.com/
NumberMSR-TR-2008-163
Pages18
InstitutionMicrosoft Research
PublisherSpringer-Verlag
> Publications > Constraint-based Invariant Inference over Predicate Abstraction