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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Colón, M. A., Sankaranarayanan, S., & Sipma, H. B. (2003). Linear invariant generation using non-linear constraint solving. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2725, 420–432. https://doi.org/10.1007/978-3-540-45069-6_39
Mendeley helps you to discover research relevant for your work.