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 we 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, we show how to model the problem of
context-sensitive interprocedural program verification. We also present the first constraint …

Results Generator converts second-order logic formula based on those con straints into first-
order logic formula, then converts the first order logic formula into a quantifier-free formula,
which is then converted into a Boolean satisfiability formula. Off-the shelf constraint solvers
may then be applied to the Boolean satisfiability formula to generate program analysis
results. Various templates may be used to convert the second-order logic formula into the
first-order logic formula. Further described are interprocedural analysis and the …