Abstract
Present approaches for non-linear loop invariant generation are limited to linear (affine) systems, or they relay on non scalable methods which have high complexity. Moreover, for programs with nested loops and conditional statements that describe multivariate polynomials or multivariate fractional systems, no applicable method is known to lend itself to non-trivial non-linear invariants generation. We demonstrate a powerful computational complete method to solve this problem. Our approach avoids first-order quantifier elimination, cylindrical algebraic decomposition and Grobner bases computation, hereby circumventing difficulties met by recent methods.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Tiwari, A., Rueß, H., Saïdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 113–127. Springer, Heidelberg (2001)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Floyd, R.W.: Assigning meanings to programs. In: Proceedings of the 19th Symphosia in Applied Mathematics, pp. 19–37 (1967)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using grobner bases. In: POPL 2004: Proc. of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 318–329. ACM Press, New York (2004)
Bensalem, S., Bozga, M., Ghirvu, J.C., Lakhnech, L.: A transformation approach for generating non-linear invariants. In: Static Analysis Symposium, pp. 101–114 (2000)
Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64(1), 54–75 (2007)
Bensalem, S., Lakhnech, Y., Saidi, H.: Powerful techniques for the automatic generation of invariants. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 323–335. Springer, Heidelberg (1996)
Chen, Y., Xia, B., Yang, L., Zhan, N.: Generating polynomial invariants with discoverer and qepcad. In: Formal Methods and Hybrid Real-Time Systems, pp. 67–82 (2007)
Kovacs, L.: Reasoning algebraically about p-solvable loops. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 249–264. Springer, Heidelberg (2008)
Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005)
Rodríguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symb. Comput. 42(4), 443–476 (2007)
Weispfenning, V.: Quantifier elimination for real algebra - the quadratic case and beyond. Applicable Algebra in Engineering, Communication and Computing 8(2), 85–101 (1997)
Collins, G.E.: Quantifier Elimination for the Elementary Theory of RealClosed Fields by Cylindrical Algebraic Decomposition. LNCS. Springer, Heidelberg (1975)
Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of Logic Programming 13(2–3), 103–179 (1992)
Müller-Olm, M., Seidl, H.: Polynomial constants are decidable. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 4–19. Springer, Heidelberg (2002)
Kovacs, L., Jebelean, T.: Finding polynomial invariants for imperative loops in the theorema system. In: Proc.of Verify 2006 Workshop, pp. 52–67 (2006)
Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Proc. IMACS Intl. Conf. on Applications of Computer Algebra (2004)
Rebiha, R., Matringe, N., Vieira-Moura, A.: Non-trivial non-linear loop invariant generation. Technical-Report-IC-07-045 (December 2007)
Lang, S.: Algebra. Springer, Heidelberg (January 2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rebiha, R., Matringe, N., Vieira Moura, A. (2008). Endomorphisms for Non-trivial Non-linear Loop Invariant Generation. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds) Theoretical Aspects of Computing - ICTAC 2008. ICTAC 2008. Lecture Notes in Computer Science, vol 5160. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85762-4_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-85762-4_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85761-7
Online ISBN: 978-3-540-85762-4
eBook Packages: Computer ScienceComputer Science (R0)