Program Analysis as Constraint Solving

A constraint-based approach to invariant generation in programs translates a program into constraints that are solved using off-the-shelf constraint solvers to yield desired program invariants. In this paper, the authors show how the constraint-based approach can be used to model a wide spectrum of program analyses in an expressive domain containing disjunctions and conjunctions of linear inequalities. In particular, they show how to model the problem of context-sensitive inter-procedural program verification. They also present the first constraint-based approach to weakest precondition and strongest post-condition inference.