Linear Invariant Generation using Non-linear Constraint Solving

Michael Colon, Sriram Sankaranarayanan, Henny Sipma

We present a new method for the generation of linear invariants which reduces the problem to a non-linear constraint solving problem. Our method, based on Farkas' Lemma, synthesizes linear invariants by extracting non-linear constraints on the coefficients of a target invariant from a program. These constraints guarantee that the linear invariant is inductive. We then apply existing techniques, including specialized quantifier elimination methods over the reals, to solve these non-linear constraints. Our method has the advantage of being complete for inductive invariants.

To our knowledge, this is the first sound and complete technique for generating inductive invariants of this form. We illustrate the practicality of our method on several examples, including cases in which traditional methods based on abstract interpretation with widening fail to generate sufficiently strong invariants.

In Computer Aided Verification (CAV), LNCS 2725, Springer-Verlag, pp 420-433, 2003.

Postscript, PDF. © 2003, Springer Verlag.


© Henny Sipma / sipma@cs.stanford.edu
Last modified: Thu Jan 12 14:40:50 PDT 2004