Abstract
Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for restricted classes of loops. For the class of solvable loops, introduced by Kapur and Rodríguez-Carbonell in 2004, one can automatically compute invariants from closed-form solutions of recurrence equations that model the loop behaviour. In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops. Our approach automatically partitions the program variables and identifies the so-called defective variables that characterise unsolvability. We further present a novel technique that automatically synthesises polynomials, in the defective variables, that admit closed-form solutions and thus lead to polynomial loop invariants. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.
This research was supported by the WWTF ICT19-018 grant ProbInG, the ERC Consolidator Grant ARTIST 101002685, the Austrian FWF project W1255-N23, and the SecInt Doctoral College funded by TU Wien.
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
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
- 4.
each benchmark in Table 1 references, in parentheses, the respective example from our paper.
References
Bartocci, E., Kovács, L., Stankovic, M.: Automatic generation of moment-based invariants for Prob-solvable loops. In: Proceedings of ATVA, pp. 255–276 (2019)
Bartocci, E., Kovács, L., Stankovic, M.: Analysis of Bayesian networks via Prob-solvable loops. In: Proceedings of ICTAC, pp. 221–241 (2020)
Britton, N.F., Franks, N.R., Pratt, S.C., Seeley, T.D.: Deciding on a new home: how do honeybees agree? Proceedings of the Royal Society of London. Series B: Biological Sciences, vol. 269(1498), pp. 1383–1388 (2002)
Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification, pp. 511–526. Springer, Berlin Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_34
Chakarov, A., Voronin, Y.L., Sankaranarayanan, S.: Deductive proofs of almost sure persistence and recurrence properties. In: Proceedings of TACAS, pp. 260–279 (2016)
Dreossi, T., Dang, T., Piazza, C.: Parallelotope bundles for polynomial reachability. In: Proceedings of HSCC, pp. 297–306 (2016)
Elspas, B., Green, M., Levitt, K., Waldinger, R.: Research in Interactive Program-Proving Techniques. Technical report, SRI (1972)
Everest, G., van der Poorten, A., Shparlinski, I., Ward, T.: Recurrence Sequences, Math. Surveys Monogr., vol. 104. Amer. Math. Soc., Providence, RI (2003)
Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD, pp. 57–64 (2015)
Frohn, F., Hark, M., Giesl, J.: Termination of polynomial loops. In: Proceedings of SAS, pp. 89–112 (2020)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Hrushovski, E., Ouaknine, J., Pouly, A., Worrell, J.: Polynomial invariants for affine programs. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018). Association for Computing Machinery, New York, NY, USA, pp. 530–539 (2018). https://doi.org/10.1145/3209108.3209142
Huang, Z., Fan, C., Mereacre, A., Mitra, S., Kwiatkowska, M.Z.: Invariant verification of nonlinear hybrid automata networks of cardiac cells. In: Proceedings of CAV, pp. 373–390 (2014)
Humenberger, A., Jaroschek, M., Kovács, L.: Aligator.jl - A Julia package for loop invariant generation. In: Proceedings of CICM, pp. 111–117 (2018)
Humenberger, A., Jaroschek, M., Kovács, L.: Automated generation of non-linear loop invariants utilizing hypergeometric sequences. In: Proceedings of ISSAC, pp. 221–228 (2017)
Humenberger, A., Jaroschek, M., Kovács, L.: Invariant generation for multi-path loops with polynomial assignments. In: Proceedings of VMCAI, pp. 226–246 (2018)
Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: Proceedings of ESOP, pp. 364–389 (2016)
Katz, S., Manna, Z.: Logical analysis of programs. Commun. ACM 19(4), 188–206 (1976)
Kauers, M., Paule, P.: The Concrete Tetrahedron. Texts and Monographs in Symbolic Computation. Springer Vienna (2011). https://doi.org/10.1007/978-3-211-99314-9
Kauers, M., Zimmermann, B.: Computing the algebraic relations of C-finite sequences and Multisequences. J. Symb. Comput. 43, 787–803 (2008)
Kincaid, Z., Cyphert, J., Breck, J., Reps, T.W.: Non-linear reasoning for invariant synthesis. In: Proceedings of POPL, pp. 54:1–54:33 (2018)
Kovács, L.: Reasoning algebraically about P-solvable loops. In: Proceedings of TACAS, pp. 249–264 (2008)
Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Proceedings of CGO, pp. 75–88 (2004)
Meurer, A., et al.: SymPy: symbolic computing in Python. Peer J. Comput. Sci. 3, e103 (2017)
Moosbrugger, M., Stankovic, M., Bartocci, E., Kovács, L.: This is the moment for probabilistic loops. CoRR abs/2204.07185 (2022). To appear in the proceedings of OOPSLA 2022
Müller-Olm, M., Seidl, H.: Computing polynomial program invariants. Inf. Process. Lett. 91(5), 233–244 (2004)
de Oliveira, S., Bensalem, S., Prevosto, V.: Polynomial invariants by linear algebra. In: Proceedings of ATVA, pp. 479–494 (2016)
Rodríguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symb. Comput. 443–476 (2007)
Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: algebraic foundations. In: Proceedings of ISSAC, p. 266–273 (2004)
Sankaranarayanan, S., Chou, Y., Goubault, E., Putot, S.: Reasoning about uncertainties in discrete-time dynamical systems using polynomial forms. In: Proceedings of NeurIPS, pp. 17502–17513 (2020)
Schreuder, A., Ong, C.L.: Polynomial Probabilistic Invariants and the Optional Stopping Theorem. CoRR abs/1910.12634 (2019)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Amrollahi, D., Bartocci, E., Kenison, G., Kovács, L., Moosbrugger, M., Stankovič, M. (2022). Solving Invariant Generation for Unsolvable Loops. In: Singh, G., Urban, C. (eds) Static Analysis. SAS 2022. Lecture Notes in Computer Science, vol 13790. Springer, Cham. https://doi.org/10.1007/978-3-031-22308-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-031-22308-2_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-22307-5
Online ISBN: 978-3-031-22308-2
eBook Packages: Computer ScienceComputer Science (R0)