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 cases in which traditional methods based on abstract interpretation with widening fail to generate sufficiently strong invariants.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Besson, F., Jensen, T., Talpin, J.-P.: Polyhedral analysis for synchronous languages. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 51–69. Springer, Heidelberg (1999)
Bockmayr, A., Weispfenning, V.: Solving numerical constraints. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 12, vol. I, pp. 751–842. Elsevier Science, Amsterdam (2001)
Clarke, E.M.: Synthesis of resource invariants for concurrent programs. In: ACM Principles of Programming Languages, pp. 211–221 (January 1979)
Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation 12(3), 299–328 (1991)
Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. LNCS, vol. 33, pp. 134–183 (1975)
Cousot, P., Cousot, R.: Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM Principles of Programming Languages, pp. 238–252 (1977)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the variables of a program. In: ACM Principles of Programming Languages, pp. 84–97 (January 1978)
Dolzmann, A., Sturm, T.: REDLOG: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31(2), 2–9 (1997)
Fukuda, K., Prodon, A.: Double description method revisited. In: Deza, M., Manoussakis, I., Euler, R. (eds.) CCS 1995. LNCS, vol. 1120, pp. 91–111. Springer, Heidelberg (1996)
Halbwachs, N., Proy, Y.-E.: POLyhedra desK cAlculator (POLKA). In: VERIMAG, Montbonnot, France (September 1995)
Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11(2), 157–185 (1997)
Henzinger, T.A., Ho, P.-H.: Model-checking strategies for hybrid systems. In: Conference on Industrial and Engineering Applications of AI and Expert Systems (1994)
Henzinger, T.A., Ho, P.-H.: Algorithmic analysis of nonlinear hybrid systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 225–238. Springer, Heidelberg (1995)
Hong, H.: RISC-CLP(Real): Constraint logic programming over real numbers. In: CLP: Selected Research. MIT Press, Cambridge (1993)
Jaffar, J., Lassez, J.-L.: Constraint logic programming. In: Principles of Programming Languages (popl), pp. 111–119 (January 1987)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)
Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1986)
Tarski, A.: A decision method for elementary algebra and geometry, vol. 5. Univ. of California Press, Berkeley (1951)
Weispfenning, V.: Quantifier elimination for real algebra—the quadratic case and beyond. In: Applied Algebra and Error-Correcting Codes (AAECC) 8, pp. 85–101 (1997)
Wirth, N.: Algorithms + Data Structures = Programs. Prentice-Hall, Englewood Cliffs (1976)
Zippel, R.: Effective Polynomial Computation. Kluwer Academic Publishers, Boston (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Colón, M.A., Sankaranarayanan, S., Sipma, H.B. (2003). Linear Invariant Generation Using Non-linear Constraint Solving. In: Hunt, W.A., Somenzi, F. (eds) Computer Aided Verification. CAV 2003. Lecture Notes in Computer Science, vol 2725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45069-6_39
Download citation
DOI: https://doi.org/10.1007/978-3-540-45069-6_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40524-5
Online ISBN: 978-3-540-45069-6
eBook Packages: Springer Book Archive