Abstract
Program analysis requires the generation of program properties expressing conditions to hold at intermediate program locations. When it comes to programs with loops, these properties are typically expressed as loop invariants. In this paper we study a class of multi-path program loops with numeric variables, in particular nested loops with conditionals, where assignments to program variables are polynomial expressions over program variables. We call this class of loops extended P-solvable and introduce an algorithm for generating all polynomial invariants of such loops. By an iterative procedure employing Gröbner basis computation, our approach computes the polynomial ideal of the polynomial invariants of each program path and combines these ideals sequentially until a fixed point is reached. This fixed point represents the polynomial ideal of all polynomial invariants of the given extended P-solvable loop. We prove termination of our method and show that the maximal number of iterations for reaching the fixed point depends linearly on the number of program variables and the number of inner loops. In particular, for a loop with m program variables and r conditional branches we prove an upper bound of \(m\cdot r\) iterations. We implemented our approach in the Aligator software package. Furthermore, we evaluated it on 18 programs with polynomial arithmetic and compared it to existing methods in invariant generation. The results show the efficiency of our approach.
L. Kovács—All authors are supported by the ERC Starting Grant 2014 SYMCAR 639270. Furthermore, we acknowledge funding from the Wallenberg Academy Fellowship 2014 TheProSE, the Swedish VR grant GenPro D0497701, and the Austrian FWF research project RiSE S11409-N23. We also acknowledge support from the FWF project W1255-N23.
Access provided by CONRICYT-eBooks. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Buchberger, B.: An Algorithm for Finding the Basis Elements of the Residue Class Ring of a Zero Dimensional Polynomial Ideal. J. Symbolic Computation 41(3–4), 475–511 (2006)
Cachera, D., Jensen, T., Jobin, A., Kirchner, F.: Inference of polynomial invariants for imperative programs: a farewell to gröbner bases. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 58–74. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33125-1_7
Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: Proc. of FMCAD, pp. 57–64. FMCAD Inc, Austin (2015)
Humenberger, A., Jaroschek, M., Kovács, L.: Automated generation of non-linear loop invariants utilizing hypergeometric Sequences. In: Proceedings of the 2017 ACM on International Symposium on Symbolic and Algebraic Computation, ISSAC 2017, pp. 221–228. ACM, New York (2017)
Kauers, M., Paule, P.: The Concrete Tetrahedron. Text and Monographs in Symbolic Computation, 1st edn. Springer, Wien (2011)
Kauers, M., Zimmermann, B.: Computing the algebraic relations of C-finite sequences and multisequences. Journal of Symbolic Computation 43(11), 787–803 (2008)
Kincaid, Z., Cyphert, J., Breck, J., Reps, T.: Non-linear reasoning for invariant synthesis. In: POPL (2018) (to appear)
Kovács, L.: Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. Ph.D. thesis, RISC, Johannes Kepler University Linz, October 2007
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). https://doi.org/10.1007/978-3-540-78800-3_18
Kovács, L.: A complete invariant generation approach for P-solvable loops. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 242–256. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11486-1_21
Müller-Olm, M., Seidl, H.: A note on karr’s algorithm. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1016–1028. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27836-8_85
de Oliveira, S., Bensalem, S., Prevosto, V.: Polynomial invariants by linear algebra. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 479–494. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_30
Paule, P., Schorn, M.: A Mathematica Version of Zeilberger’s Algorithm for Proving Binomial Coefficient Identities. Journal of Symbolic Computation 20, 673–698 (1995)
Petkovšek, M.: Mathematic package hyper (1998). http://www.fmf.uni-lj.si/~petkovsek/
Research Institute for Symbolic Computation: Mathematic Package ErgoSum (2016). http://www.risc.jku.at/research/combinat/software/ergosum/
Rodriguez-Carbonell, E., Kapur, D.: Automatic Generation of Polynomial Invariants of Bounded Degree using Abstract Interpretation. J. Science of Computer Programming 64(1), 54–75 (2007)
Rodríguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. Journal of Symbolic Computation 42(4), 443–476 (2007)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using gröbner bases. In: Proc. of POPL, pp. 318–329. ACM, New York (2004)
Schneider, C.: Summation theory ii: Characterizations of \(r\pi \sigma \)-extensions and algorithmic aspects. J. Symb. Comput. 80(3), 616–664 (2017). arXiv:1603.04285 [cs.SC]
Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 574–592. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_31
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Humenberger, A., Jaroschek, M., Kovács, L. (2018). Invariant Generation for Multi-Path Loops with Polynomial Assignments. In: Dillig, I., Palsberg, J. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2018. Lecture Notes in Computer Science(), vol 10747. Springer, Cham. https://doi.org/10.1007/978-3-319-73721-8_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-73721-8_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-73720-1
Online ISBN: 978-3-319-73721-8
eBook Packages: Computer ScienceComputer Science (R0)