Linear Invariant Generation using Non-Linear Constraint SolvingMichael 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 2003), Lecture Notes in Computer Science, vol. 2725, pp. 420-432, 2003. |
| © 2003, Springer Verlag |
|
postscript
pdf
|