Sciweavers

CAV
2003
Springer

Linear Invariant Generation Using Non-linear Constraint Solving

14 years 5 months ago
Linear Invariant Generation Using Non-linear Constraint Solving
Abstract. 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 which traditional methods based on abstract interpretation with widening fail to generate sufficiently strong invariants.
Michael Colón, Sriram Sankaranarayanan, Hen
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where CAV
Authors Michael Colón, Sriram Sankaranarayanan, Henny Sipma
Comments (0)