{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:50:43Z","timestamp":1770277843371,"version":"3.49.0"},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ANR","award":["ANR-22-CE48-0005"],"award-info":[{"award-number":["ANR-22-CE48-0005"]}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["ARTIST 101002685"],"award-info":[{"award-number":["ARTIST 101002685"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["10.47379\/ICT19018"],"award-info":[{"award-number":["10.47379\/ICT19018"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"publisher","award":["Frontier Research Grant EP\/X033813\/1"],"award-info":[{"award-number":["Frontier Research Grant EP\/X033813\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"publisher"}]},{"name":"CNRS","award":["International Emerging Actions"],"award-info":[{"award-number":["International Emerging Actions"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>The automatic generation of loop invariants is a fundamental challenge in software verification. While this task is undecidable in general, it is decidable for certain restricted classes of programs. This work focuses on invariant generation for (branching-free) loops with a single linear update.<\/jats:p>\n                  <jats:p>Our primary contribution is a polynomial-space algorithm that computes the strongest algebraic invariant for simple linear loops, generating all polynomial equations that hold among program variables across all reachable states. The key to achieving our complexity bounds lies in mitigating the blow-up associated with variable elimination and Gr\u00f6bner basis computation, as seen in prior works. Our procedure runs in polynomial time when the number of program variables is fixed.<\/jats:p>\n                  <jats:p>We examine various applications of our results on invariant generation, focusing on invariant verification and loop synthesis. The invariant verification problem investigates whether a polynomial ideal defining an algebraic set serves as an invariant for a given linear loop. We show that this problem is coNP-complete and lies in PSPACE when the input ideal is given in dense or sparse representations, respectively. In the context of loop synthesis, we aim to construct a loop with an infinite set of reachable states that upholds a specified algebraic property as an invariant. The strong synthesis variant of this problem requires the construction of loops for which the given property is the strongest invariant. In terms of hardness, synthesising loops over integers (or rationals) is as hard as Hilbert\u2019s Tenth problem (or its analogue over the rationals). When the constants of the output are constrained to bit-bounded rational numbers, we demonstrate that loop synthesis and its strong variant are both decidable in PSPACE, and in NP when the number of program variables is fixed.<\/jats:p>","DOI":"10.1145\/3704862","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"745-771","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Simple Linear Loops: Algebraic Invariants and Applications"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6228-9071","authenticated-orcid":false,"given":"Rida","family":"Ait El Manssour","sequence":"first","affiliation":[{"name":"CNRS - IRIF, Paris, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7661-7061","authenticated-orcid":false,"given":"George","family":"Kenison","sequence":"additional","affiliation":[{"name":"Liverpool John Moores University, Liverpool, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7779-2339","authenticated-orcid":false,"given":"Mahsa","family":"Shirmohammadi","sequence":"additional","affiliation":[{"name":"CNRS - IRIF, Paris, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5758-0657","authenticated-orcid":false,"given":"Anton","family":"Varonka","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"crossref","unstructured":"Rida Ait El Manssour George Kenison Mahsa Shirmohammadi and Anton Varonka. 2024. Simple linear loops: algebraic invariants and applications. (2024). arXiv:2407.09154v2 [cs.CC].","DOI":"10.1145\/3704862"},{"key":"e_1_3_1_3_2","unstructured":"Rida Ait El Manssour George Kenison Mahsa Shirmohammadi and James Worrell. 2024. Determination problems for orbit closures and matrix groups. (2024). arXiv:2407.04626 [cs.CC]."},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1137\/070697926"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3208071"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-024-00455-0"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","unstructured":"Daneshvar Amrollahi Ezio Bartocci George Kenison Laura Kov\u00e1cs Marcel Moosbrugger and Miroslav Stankovic. 2022. Solving Invariant Generation for Unsolvable Loops. In Static Analysis 19\u201343. https:\/\/doi.org\/10.1007\/978-3-031-22308-2_3 10.1007\/978-3-031-22308-2_3","DOI":"10.1007\/978-3-031-22308-2_3"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.5555\/1540612"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(88)90028-1"},{"key":"e_1_3_1_10_2","doi-asserted-by":"crossref","unstructured":"Nikhil Balaji Klara Nosan Mahsa Shirmohammadi and James Worrell. 2022. Identity testing for radical expressions. In LICS \u201922: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science Haifa Israel August 2 - 5 2022 8:1\u20138:11.","DOI":"10.1145\/3531130.3533331"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","unstructured":"Nikhil Balaji Sylvain Perifel Mahsa Shirmohammadi and James Worrell. 2021. Cyclotomic identity testing and applications. In ISSAC \u201921: International Symposium on Symbolic and Algebraic Computation Virtual Event Russia July 18-23 2021 35\u201342. https:\/\/doi.org\/10.1145\/3452143.3465530 10.1145\/3452143.3465530","DOI":"10.1145\/3452143.3465530"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","unstructured":"Erdenebayar Bayarmagnai Fatemeh Mohammadi and R\u00e9mi Pr\u00e9bet. 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 10.1145\/3666000.3669710","DOI":"10.1145\/3666000.3669710"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1090\/bull\/1665"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005101"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_27"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Markus Bl\u00e4ser Christian Ikenmeyer Vladimir Lysikov Anurag Pandey and Frank-Olaf Schreyer. 2021. On the orbit closure containment problem and slice rank of tensors. In Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms SODA 2021 Virtual Conference January 10 - 13 2021 2565\u20132584. https:\/\/doi.org\/10.1137\/1.9781611976465.152 10.1137\/1.9781611976465.152","DOI":"10.1137\/1.9781611976465.152"},{"key":"e_1_3_1_17_2","volume-title":"Heights in Diophantine geometry. Number 4","author":"Bombieri Enrico","year":"2006","unstructured":"Enrico Bombieri and Walter Gubler. 2006. Heights in Diophantine geometry. Number 4. Cambridge university press."},{"key":"e_1_3_1_18_2","article-title":"Completeness classes in algebraic complexity theory","author":"B\u00fcrgisser Peter","year":"2024","unstructured":"Peter B\u00fcrgisser. 2024. Completeness classes in algebraic complexity theory. arXiv preprint arXiv:2406.06217.","journal-title":"arXiv preprint arXiv:2406.06217"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1137\/090765328"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054194000165"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794276853"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/tit.2010.2044061"},{"key":"e_1_3_1_23_2","volume-title":"A course in computational algebraic number theory","author":"Cohen Henri","year":"2013","unstructured":"Henri Cohen. 2013. A course in computational algebraic number theory. Vol. 138. Springer Science & Business Media."},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-16721-3"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632867"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80004-X"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1972-0304347-1"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1201\/9781315120140"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2004.11.008"},{"key":"e_1_3_1_30_2","doi-asserted-by":"crossref","unstructured":"Klaus Dr\u00e4ger. 2016. The invariance problem for matrix semigroups. In Foundations of Software Science and Computation Structures 479\u2013492.","DOI":"10.1007\/978-3-662-49630-5_28"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40328-6_37"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.13137\/2464-8728\/33099"},{"key":"e_1_3_1_33_2","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness (Series of Books in the Mathematical Sciences)","author":"Garey M. R.","year":"1979","unstructured":"M. R. Garey and D. S. Johnson. 1979. Computers and Intractability: A Guide to the Theory of NP-Completeness (Series of Books in the Mathematical Sciences). (First Edition ed.). W. H. Freeman."},{"key":"e_1_3_1_34_2","volume-title":"Algorithms Related to Multiplicative Representations of Algebraic Numbers","author":"Ge Guoqiang","year":"1993","unstructured":"Guoqiang Ge. 1993. Algorithms Related to Multiplicative Representations of Algebraic Numbers. Ph.D. Dissertation. U.C. Berkeley."},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/138859.138867"},{"key":"e_1_3_1_36_2","unstructured":"Daniel R. Grayson and Michael E. Stillman. 2002. Macaulay2 a software system for research in algebraic geometry. Available at http:\/\/www2.macaulay2.com. (2002)."},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","unstructured":"S. Hitarth George Kenison Laura Kov\u00e1cs and Anton Varonka. 2024. Linear Loop Synthesis for Quadratic Invariants. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Vol. 289 41:1\u201341:18. https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2024.41 10.4230\/LIPIcs.STACS.2024.41","DOI":"10.4230\/LIPIcs.STACS.2024.41"},{"key":"e_1_3_1_39_2","unstructured":"Mehran Hosseini Jo\u00ebl Ouaknine and James Worrell. 2019. Termination of linear loops over the integers. In 46th International Colloquium on Automata Languages and Programming ICALP 2019 July 9-12 2019 Patras Greece. Vol. 132 118:1\u2013118:13."},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3614319"},{"key":"e_1_3_1_41_2","doi-asserted-by":"crossref","unstructured":"Ehud Hrushovski Jo\u00ebl Ouaknine Amaury Pouly and James Worrell. 2018. Polynomial invariants for affine programs. In Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science LICS 2018 Oxford UK July 09-12 2018 530\u2013539.","DOI":"10.1145\/3209108.3209142"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527458"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","unstructured":"Andreas Humenberger Nikolaj S. Bj\u00f8rner and Laura Kov\u00e1cs. 2020. Algebra-Based Loop Synthesis. In Integrated Formal Methods - 16th International Conference IFM 2020 Lugano Switzerland November 16-20 2020 Proceedings. Vol. 12546 440\u2013459. https:\/\/doi.org\/10.1007\/978-3-030-63461-2\\_24 10.1007\/978-3-030-63461-2\\_24","DOI":"10.1007\/978-3-030-63461-2\\_24"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","unstructured":"Andreas Humenberger Maximilian Jaroschek and Laura Kov\u00e1cs. 2017. Automated generation of non-linear loop invariants utilizing hypergeometric sequences. In Proceedings of the 2017 ACM on International Symposium on Symbolic and Algebraic Computation 221\u2013228. https:\/\/doi.org\/10.1145\/3087604.3087623 10.1145\/3087604.3087623","DOI":"10.1145\/3087604.3087623"},{"key":"e_1_3_1_45_2","doi-asserted-by":"crossref","unstructured":"Andreas Humenberger Maximilian Jaroschek and Laura Kov\u00e1cs. 2018. Invariant generation for multi-path loops with polynomial assignments. In Verification Model Checking and Abstract Interpretation 226\u2013246.","DOI":"10.1007\/978-3-319-73721-8_11"},{"key":"e_1_3_1_46_2","doi-asserted-by":"crossref","unstructured":"Charles R Johnson. 1990. Matrix completion problems: a survey. In Matrix theory and applications. Vol. 40 171\u2013198.","DOI":"10.1090\/psapm\/040\/1059486"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/1240233.1240241"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.05.001"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2008.03.002"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","unstructured":"George Kenison Laura Kov\u00e1cs and Anton Varonka. 2023. From Polynomial Invariants to Linear Loops. In Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation ISSAC 2023 Troms\u00f8 Norway July 24-27 2023 398\u2013406. https:\/\/doi.org\/10.1145\/3597066.3597109 10.1145\/3597066.3597109","DOI":"10.1145\/3597066.3597109"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"e_1_3_1_53_2","doi-asserted-by":"crossref","unstructured":"P. Koiran. 1997. Randomized and deterministic algorithms for the dimension of algebraic varieties. In 38th Annual Symposium on Foundations of Computer Science FOCS \u201997 Miami Beach Florida USA October 19-22 1997 36\u201345.","DOI":"10.1109\/SFCS.1997.646091"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1006\/jcom.1996.0019"},{"key":"e_1_3_1_55_2","doi-asserted-by":"crossref","unstructured":"Laura Kov\u00e1cs. 2008. Reasoning algebraically about p-solvable loops. In Tools and Algorithms for the Construction and Analysis of Systems 249\u2013264.","DOI":"10.1007\/978-3-540-78800-3_18"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","unstructured":"Rupak Majumdar Jo\u00ebl Ouaknine Amaury Pouly and James Worrell. 2020. Algebraic Invariants for Linear Hybrid Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Vol. 171 32:1\u201332:17. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.32 10.4230\/LIPIcs.CONCUR.2020.32","DOI":"10.4230\/LIPIcs.CONCUR.2020.32"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90044-2"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","unstructured":"D. W. Masser. 1988. Linear relations on algebraic groups. In New Advances in Transcendence Theory 248\u2013262. https:\/\/doi.org\/10.1017\/CBO9780511897184.016 10.1017\/CBO9780511897184.016","DOI":"10.1017\/CBO9780511897184.016"},{"key":"e_1_3_1_59_2","first-page":"354","article-title":"Enumerable sets are Diophantine","volume":"11","author":"Matiyasevich Yuri","year":"1970","unstructured":"Yuri Matiyasevich. 1970. Enumerable sets are Diophantine. Soviet Math. Dokl., 11, 354\u2013358.","journal-title":"Soviet Math. Dokl"},{"key":"e_1_3_1_60_2","volume-title":"Algorithmic Algebra","author":"Mishra B.","year":"2012","unstructured":"B. Mishra. 2012. Algorithmic Algebra. Springer New York."},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_85"},{"key":"e_1_3_1_62_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IPL.2004.05.004"},{"key":"e_1_3_1_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632872"},{"key":"e_1_3_1_64_2","doi-asserted-by":"crossref","unstructured":"K. Nosan A. Pouly S. Schmitz M. Shirmohammadi and J. Worrell. 2022. On the Computation of the Zariski Closure of Finitely Generated Groups of Matrices. In Proceedings of the 2022 International Symposium on Symbolic and Algebraic Computation 129\u2013138.","DOI":"10.1145\/3476446.3536172"},{"key":"e_1_3_1_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/2766189.2766191"},{"key":"e_1_3_1_66_2","doi-asserted-by":"publisher","unstructured":"Jo\u00ebl Ouaknine and James Worrell. 2014. Positivity problems for low-order linear recurrence sequences. In Proceedings of the 2014 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA) 366\u2013379. https:\/\/doi.org\/10.1137\/1.9781611973402.27 10.1137\/1.9781611973402.27","DOI":"10.1137\/1.9781611973402.27"},{"key":"e_1_3_1_67_2","first-page":"3","article-title":"Undecidability in number theory","volume":"55","author":"Poonen Bjorn","year":"2008","unstructured":"Bjorn Poonen. 2008. Undecidability in number theory. Notices of the AMS, 55, 3.","journal-title":"Notices of the AMS"},{"key":"e_1_3_1_68_2","doi-asserted-by":"crossref","unstructured":"Enric Rodr\u00edguez-Carbonell and Deepak Kapur. 2004. Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations. In Proc. of ISSAC 266\u2013273.","DOI":"10.1145\/1005285.1005324"},{"key":"e_1_3_1_69_2","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1305810912"},{"key":"e_1_3_1_70_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-69904-2"},{"key":"e_1_3_1_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0223-4"},{"key":"e_1_3_1_72_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90135-0"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704862","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704862","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:50Z","timestamp":1770200210000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704862"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":71,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704862"],"URL":"https:\/\/doi.org\/10.1145\/3704862","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}