{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T12:18:44Z","timestamp":1768738724359,"version":"3.49.0"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2024,6,11]],"date-time":"2024-06-11T00:00:00Z","timestamp":1718064000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,6,11]],"date-time":"2024-06-11T00:00:00Z","timestamp":1718064000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"TU Wien"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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 <jats:italic>solvable<\/jats:italic> loops, introduced by Rodr\u00edguez-Carbonell and Kapur (in: Proceedings of the ISSAC, pp 266\u2013273, 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 <jats:italic>unsolvable<\/jats:italic> loops. Our approach automatically partitions the program variables and identifies the so-called <jats:italic>defective<\/jats:italic> variables that characterise unsolvability. Herein we consider the following two applications. First, we present a novel technique that automatically synthesises polynomials from defective monomials, that admit closed-form solutions and thus lead to polynomial loop invariants. Second, given an unsolvable loop, we synthesise solvable loops with the following property: the invariant polynomials of the solvable loops are all invariants of the given unsolvable loop. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.<\/jats:p>","DOI":"10.1007\/s10703-024-00455-0","type":"journal-article","created":{"date-parts":[[2024,6,11]],"date-time":"2024-06-11T11:14:12Z","timestamp":1718104452000},"page":"163-194","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["(Un)Solvable loop analysis"],"prefix":"10.1007","volume":"65","author":[{"given":"Daneshvar","family":"Amrollahi","sequence":"first","affiliation":[]},{"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[]},{"given":"George","family":"Kenison","sequence":"additional","affiliation":[]},{"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[]},{"given":"Marcel","family":"Moosbrugger","sequence":"additional","affiliation":[]},{"given":"Miroslav","family":"Stankovi\u010d","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,6,11]]},"reference":[{"key":"455_CR1","doi-asserted-by":"publisher","unstructured":"Amrollahi D, Bartocci E, Kenison G, Kov\u00e1cs L, Moosbrugger M, Stankovic M (2022) Solving invariant generation for unsolvable loops. In: Singh G, Urban C (eds) Static analysis\u201429th international symposium, SAS 2022, Auckland, New Zealand, December 5\u20137, 2022, proceedings. Lecture notes in computer science, vol 13790, pp 19\u201343. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-031-22308-2_3","DOI":"10.1007\/978-3-031-22308-2_3"},{"key":"455_CR2","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez-Carbonell E, Kapur D (2004) Automatic generation of polynomial loop invariants: algebraic foundations. In: Proceedings of the ISSAC, pp 266\u2013273","DOI":"10.1145\/1005285.1005324"},{"key":"455_CR3","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs L (2008) Reasoning algebraically about P-solvable loops. In: Proceedings of the TACAS, pp 249\u2013264","DOI":"10.1007\/978-3-540-78800-3_18"},{"key":"455_CR4","doi-asserted-by":"crossref","unstructured":"Oliveira S, Bensalem S, Prevosto V (2016) Polynomial invariants by linear algebra. In: Proceedings of the ATVA, pp 479\u2013494","DOI":"10.1007\/978-3-319-46520-3_30"},{"key":"455_CR5","doi-asserted-by":"crossref","unstructured":"Kincaid Z, Cyphert J, Breck J, Reps TW (2018) Non-linear reasoning for invariant synthesis. In: Proceedings of the POPL, pp 54\u201315433","DOI":"10.1145\/3158142"},{"key":"455_CR6","doi-asserted-by":"crossref","unstructured":"Humenberger A, Jaroschek M, Kov\u00e1cs L (2018) Invariant generation for multi-path loops with polynomial assignments. In: Proceedings of the VMCAI, pp 226\u2013246","DOI":"10.1007\/978-3-319-73721-8_11"},{"key":"455_CR7","doi-asserted-by":"crossref","unstructured":"Huang Z, Fan C, Mereacre A, Mitra S, Kwiatkowska MZ (2014) Invariant verification of nonlinear hybrid automata networks of cardiac cells. In: Proceedings of the CAV, pp 373\u2013390","DOI":"10.1007\/978-3-319-08867-9_25"},{"key":"455_CR8","doi-asserted-by":"crossref","unstructured":"Kaminski BL, Katoen J, Matheja C, Olmedo F (2016) Weakest precondition reasoning for expected run-times of probabilistic programs. In: Proceedings of the ESOP, pp 364\u2013389","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"455_CR9","doi-asserted-by":"crossref","unstructured":"Bartocci E, Kov\u00e1cs L, Stankovic M (2019) Automatic generation of moment-based invariants for prob-solvable loops. In: Proceedings of the ATVA, pp 255\u2013276","DOI":"10.1007\/978-3-030-31784-3_15"},{"issue":"5","key":"455_CR10","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.ipl.2004.05.004","volume":"91","author":"M M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm M, Seidl H (2004) Computing polynomial program invariants. Inf Process Lett 91(5):233\u2013244","journal-title":"Inf Process Lett"},{"key":"455_CR11","unstructured":"Hrushovski E, Ouaknine J, Pouly A, Worrell J (2020) On strongest algebraic program invariants. J ACM (to appear)"},{"key":"455_CR12","unstructured":"Elspas B, Green M, Levitt K, Waldinger R (1972) Research in interactive program-proving techniques. Technical report, SRI"},{"issue":"4","key":"455_CR13","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1145\/360032.360048","volume":"19","author":"S Katz","year":"1976","unstructured":"Katz S, Manna Z (1976) Logical analysis of programs. Commun ACM 19(4):188\u2013206","journal-title":"Commun ACM"},{"key":"455_CR14","series-title":"Mathematical surveys and monographs","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1090\/surv\/104","volume-title":"Recurrence sequences","author":"G Everest","year":"2003","unstructured":"Everest G, Poorten A, Shparlinski I, Ward T (2003) Recurrence sequences, vol 104. Mathematical surveys and monographs. American Mathematical Society, Providence, p 318"},{"key":"455_CR15","series-title":"Texts and monographs in symbolic computation","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-7091-0445-3","volume-title":"The concrete tetrahedron","author":"M Kauers","year":"2011","unstructured":"Kauers M, Paule P (2011) The concrete tetrahedron. Texts and monographs in symbolic computation. Springer, Vienna, p 203"},{"key":"455_CR16","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1016\/j.jsc.2007.01.002","volume":"42","author":"E Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell E, Kapur D (2007) Generating all polynomial invariants in simple loops. J Symb Comput 42:443\u2013476","journal-title":"J Symb Comput"},{"key":"455_CR17","doi-asserted-by":"crossref","unstructured":"Farzan A, Kincaid Z (2015) Compositional recurrence analysis. In: FMCAD, pp 57\u201364","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"455_CR18","doi-asserted-by":"crossref","unstructured":"Bartocci E, Kov\u00e1cs L, Stankovic M (2020) Analysis of Bayesian networks via prob-solvable loops. In: Proceedings of the ICTAC, pp 221\u2013241","DOI":"10.1007\/978-3-030-64276-1_12"},{"key":"455_CR19","doi-asserted-by":"crossref","unstructured":"Frohn F, Hark M, Giesl J (2020) Termination of polynomial loops. In: Proceedings of the SAS, pp 89\u2013112 (2020)","DOI":"10.1007\/978-3-030-65474-0_5"},{"key":"455_CR20","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-39799-8_34","volume-title":"Computer aided verification","author":"A Chakarov","year":"2013","unstructured":"Chakarov A, Sankaranarayanan S (2013) Probabilistic program analysis with martingales. In: Sharygina N, Veith H (eds) Computer aided verification. Springer, Berlin, pp 511\u2013526"},{"key":"455_CR21","doi-asserted-by":"crossref","unstructured":"Lattner C, Adve VS (2004) LLVM: a compilation framework for lifelong program analysis and transformation. In: Proceedings of the CGO, pp 75\u201388","DOI":"10.1109\/CGO.2004.1281665"},{"issue":"10","key":"455_CR22","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580","journal-title":"Commun ACM"},{"key":"455_CR23","doi-asserted-by":"publisher","first-page":"787","DOI":"10.1016\/j.jsc.2008.03.002","volume":"43","author":"M Kauers","year":"2008","unstructured":"Kauers M, Zimmermann B (2008) Computing the algebraic relations of C-finite sequences and multisequences. J Symb Comput 43:787\u2013803","journal-title":"J Symb Comput"},{"key":"455_CR24","doi-asserted-by":"crossref","unstructured":"Humenberger A, Jaroschek M, Kov\u00e1cs L (2017) Automated generation of non-linear loop invariants utilizing hypergeometric sequences. In: Proceedings of the ISSAC, pp 221\u2013228","DOI":"10.1145\/3087604.3087623"},{"key":"455_CR25","unstructured":"Schreuder A, Ong C-L (2019) Polynomial probabilistic invariants and the optional stopping theorem. CoRR. arXiv:1910.12634"},{"key":"455_CR26","doi-asserted-by":"crossref","unstructured":"Chakarov A, Voronin Y-L, Sankaranarayanan S (2016) Deductive proofs of almost sure persistence and recurrence properties. In: Proceedings of the TACAS, pp 260\u2013279","DOI":"10.1007\/978-3-662-49674-9_15"},{"key":"455_CR27","doi-asserted-by":"publisher","DOI":"10.1038\/261459a0","author":"RM May","year":"1976","unstructured":"May RM (1976) Simple mathematical models with very complicated dynamics. Nature. https:\/\/doi.org\/10.1038\/261459a0","journal-title":"Nature"},{"issue":"1063\/1","key":"455_CR28","first-page":"5125097","volume":"10","author":"MF Maritz","year":"2020","unstructured":"Maritz MF (2020) A note on exact solutions of the logistic map. Chaos Interdiscip J Nonlinear Sci 10(1063\/1):5125097","journal-title":"Chaos Interdiscip J Nonlinear Sci"},{"key":"455_CR29","doi-asserted-by":"publisher","DOI":"10.1145\/3563341","author":"M Moosbrugger","year":"2022","unstructured":"Moosbrugger M, Stankovi\u010d M, Bartocci E, Kov\u00e1cs L (2022) This is the moment for probabilistic loops. Proc ACM Program Lang. https:\/\/doi.org\/10.1145\/3563341","journal-title":"Proc ACM Program Lang"},{"issue":"1498","key":"455_CR30","doi-asserted-by":"publisher","first-page":"1383","DOI":"10.1098\/rspb.2002.2001","volume":"269","author":"NF Britton","year":"2002","unstructured":"Britton NF, Franks NR, Pratt SC, Seeley TD (2002) Deciding on a new home: How do honeybees agree? Proc R Soc Lond Ser B Biol Sci 269(1498):1383\u20131388","journal-title":"Proc R Soc Lond Ser B Biol Sci"},{"key":"455_CR31","doi-asserted-by":"crossref","unstructured":"Dreossi T, Dang T, Piazza C (2016) Parallelotope bundles for polynomial reachability. In: Proceedings of the HSCC, pp 297\u2013306","DOI":"10.1145\/2883817.2883838"},{"key":"455_CR32","unstructured":"Sankaranarayanan S, Chou Y, Goubault E, Putot S (2020) Reasoning about uncertainties in discrete-time dynamical systems using polynomial forms. In: Proceedings of the NeurIPS, pp 17502\u201317513"},{"issue":"6\u20137","key":"455_CR33","doi-asserted-by":"publisher","first-page":"1527","DOI":"10.1142\/S021797929300247X","volume":"7","author":"M Baake","year":"1993","unstructured":"Baake M, Grimm U, Joseph D (1993) Trace maps, invariants, and some of their applications. Int J Mod Phys B 7(6\u20137):1527\u20131550. https:\/\/doi.org\/10.1142\/S021797929300247X","journal-title":"Int J Mod Phys B"},{"issue":"3\u20134","key":"455_CR34","doi-asserted-by":"publisher","first-page":"829","DOI":"10.1007\/BF02188581","volume":"74","author":"JAG Roberts","year":"1994","unstructured":"Roberts JAG, Baake M (1994) Trace maps as 3D reversible dynamical systems with an invariant. J Stat Phys 74(3\u20134):829\u2013888. https:\/\/doi.org\/10.1007\/BF02188581","journal-title":"J Stat Phys"},{"key":"455_CR35","unstructured":"Cassels JWS (1972) An introduction to diophantine approximation. Cambridge tracts in mathematics and mathematical physics, No. 45. Hafner Publishing Co., New York, p 169. Facsimile reprint of the 1957 edition"},{"issue":"5","key":"455_CR36","first-page":"141","volume":"21","author":"AV Jag\u017eev","year":"1980","unstructured":"Jag\u017eev AV (1980) On a problem of O.-H. Keller. Sibirsk Mat Zh 21(5):141\u2013150191","journal-title":"Sibirsk Mat Zh"},{"issue":"2","key":"455_CR37","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1090\/S0273-0979-1982-15032-7","volume":"7","author":"H Bass","year":"1982","unstructured":"Bass H, Connell EH, Wright D (1982) The Jacobian conjecture: reduction of degree and formal expansion of the inverse. Bull Am Math Soc 7(2):287\u2013330. https:\/\/doi.org\/10.1090\/S0273-0979-1982-15032-7","journal-title":"Bull Am Math Soc"},{"issue":"10","key":"455_CR38","doi-asserted-by":"publisher","first-page":"2849","DOI":"10.1090\/S0002-9939-06-08335-3","volume":"134","author":"M Bondt","year":"2006","unstructured":"Bondt M (2006) Quasi-translations and counterexamples to the homogeneous dependence problem. Proc Am Math Soc 134(10):2849\u20132856. https:\/\/doi.org\/10.1090\/S0002-9939-06-08335-3","journal-title":"Proc Am Math Soc"},{"key":"455_CR39","first-page":"99","volume":"46","author":"G Zampieri","year":"2008","unstructured":"Zampieri G (2008) Homogeneous polynomial invariants for cubic-homogeneous functions. Univ Iagel Acta Math 46:99\u2013103","journal-title":"Univ Iagel Acta Math"},{"key":"455_CR40","first-page":"7","volume":"46","author":"R Santos Freire Jr","year":"2008","unstructured":"Santos Freire R Jr, Gorni G, Zampieri G (2008) Search for homogeneous polynomial invariants and a cubic-homogeneous mapping without quadratic invariants. Univ Iagel Acta Math 46:7\u201313","journal-title":"Univ Iagel Acta Math"},{"key":"455_CR41","unstructured":"Nagata M (1972) On automorphism group of $$k[x,\\,y]$$. Kinokuniya Book Store Co., Ltd., Tokyo, p 53. Department of Mathematics, Kyoto University, Lectures in Mathematics, No. 5"},{"issue":"1","key":"455_CR42","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/S0021-8693(03)00424-1","volume":"269","author":"A van den Essen","year":"2003","unstructured":"van den Essen A, Peretz R (2003) Polynomial automorphisms and invariants. J Algebra 269(1):317\u2013328. https:\/\/doi.org\/10.1016\/S0021-8693(03)00424-1","journal-title":"J Algebra"},{"key":"455_CR43","doi-asserted-by":"publisher","first-page":"103","DOI":"10.7717\/peerj-cs.103","volume":"3","author":"A Meurer","year":"2017","unstructured":"Meurer A, Smith CP, Paprocki M, \u010cert\u00edk O, Kirpichev SB, Rocklin M, Kumar A, Ivanov S, Moore JK, Singh S, Rathnayake T, Vig S, Granger BE, Muller RP, Bonazzi F, Gupta H, Vats S, Johansson F, Pedregosa F, Curry MJ, Terrel AR, Rou\u010dka V, Saboo A, Fernando I, Kulal S, Cimrman R, Scopatz A (2017) SymPy: symbolic computing in Python. PeerJ Comput Sci 3:103","journal-title":"PeerJ Comput Sci"},{"key":"455_CR44","doi-asserted-by":"crossref","unstructured":"Humenberger A, Jaroschek M, Kov\u00e1cs L (2018) Aligator.jl\u2014A Julia package for loop invariant generation. In: Proceedings of the CICM, pp 111\u2013117","DOI":"10.1007\/978-3-319-96812-4_10"},{"key":"455_CR45","doi-asserted-by":"publisher","unstructured":"Bayarmagnai E, Mohammadi F, Pr\u00e9bet R (2024) Algebraic tools for computing polynomial loop invariants. In: Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation, ISSAC 2024 (To Appear). https:\/\/doi.org\/10.1145\/3666000.3669710","DOI":"10.1145\/3666000.3669710"}],"updated-by":[{"DOI":"10.1007\/s10703-024-00465-y","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2024,11,20]],"date-time":"2024-11-20T00:00:00Z","timestamp":1732060800000}}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00455-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00455-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00455-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T13:57:57Z","timestamp":1746194277000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00455-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,11]]},"references-count":45,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2025,4]]}},"alternative-id":["455"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00455-0","relation":{"correction":[{"id-type":"doi","id":"10.1007\/s10703-024-00465-y","asserted-by":"object"}]},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,11]]},"assertion":[{"value":"25 May 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 May 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 June 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 November 2024","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s10703-024-00465-y","URL":"https:\/\/doi.org\/10.1007\/s10703-024-00465-y","order":7,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}