Abstract
Automatic derivation of invariants is one of the critical conundrums in the framework of the inductive program verification methodologies. This paper presents a novel and simple approach to generating polynomial equations as loop invariants. Finite difference of expressions and linear equation solving are harnessed. Unlike related work, the generated constraints are linear equalities, which can be solved efficiently. Furthermore, invariants of higher degree can be constructed in terms of those of lower degree. The case studies demonstrate the effectiveness of the approach.
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
Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 113–129. Springer, Heidelberg (2005)
Chen, Y., Xia, B., Yang, L., Zhan, N.: Generating polynomial invariants with Discoverer and Qepcad. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems. LNCS, vol. 4700, pp. 67–82. Springer, Heidelberg (2007)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. POPL 1978, pp. 84–96 (1978)
Rodriguez-Carbonell, D.K.E.: Generating all polynomial invariants in simple loops. Journal of Symbolic Computation, 443–476 (2007)
Giacobazzi, R. (ed.): SAS 2004. LNCS, vol. 3148. Springer, Heidelberg (2004)
Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Proc. PLDI 2008, pp. 281–292 (2008)
Kovács, 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)
Michael, H.S., Colon, A., Sankaranarayanan, S.: Linear Invariant Generation Using Non-linear Constraint Solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–433. Springer, Heidelberg (2003)
Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), 31–100 (2006)
Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL, pp. 330–341 (2004a)
Müller-Olm, M., Seidl, H.: Computing polynomial program invariants. Inf. Process. Lett. 91(5), 233–244 (2004b)
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)
Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using gröbner bases. In: POPL, pp. 318–329 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, S., Li, Z., Song, X., Li, M. (2011). An Iterative Method for Generating Loop Invariants. In: Atallah, M., Li, XY., Zhu, B. (eds) Frontiers in Algorithmics and Algorithmic Aspects in Information and Management. Lecture Notes in Computer Science, vol 6681. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21204-8_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-21204-8_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21203-1
Online ISBN: 978-3-642-21204-8
eBook Packages: Computer ScienceComputer Science (R0)