{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:34:13Z","timestamp":1767929653092,"version":"3.49.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2023,10,11]],"date-time":"2023-10-11T00:00:00Z","timestamp":1696982400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ERC","award":["648701"],"award-info":[{"award-number":["648701"]}]},{"name":"DFG","award":["389792660"],"award-info":[{"award-number":["389792660"]}]},{"name":"EPSRC Fellowship","award":["EP\/N008197\/1"],"award-info":[{"award-number":["EP\/N008197\/1"]}]},{"name":"UKRI Fellowship","award":["EP\/X033813\/1"],"award-info":[{"award-number":["EP\/X033813\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2023,10,31]]},"abstract":"<jats:p>A polynomial program is one in which all assignments are given by polynomial expressions and in which all branching is nondeterministic (as opposed to conditional). Given such a program, an algebraic invariant is one that is defined by polynomial equations over the program variables at each program location. M\u00fcller-Olm and Seidl have posed the question of whether one can compute the strongest algebraic invariant of a given polynomial program. In this article, we show that, while strongest algebraic invariants are not computable in general, they can be computed in the special case of affine programs, that is, programs with exclusively linear assignments. For the latter result, our main tool is an algebraic result of independent interest: Given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate.<\/jats:p>","DOI":"10.1145\/3614319","type":"journal-article","created":{"date-parts":[[2023,8,8]],"date-time":"2023-08-08T12:01:57Z","timestamp":1691496117000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["On Strongest Algebraic Program Invariants"],"prefix":"10.1145","volume":"70","author":[{"given":"Ehud","family":"Hrushovski","sequence":"first","affiliation":[{"name":"Oxford University, UK"}]},{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems, Germany"}]},{"given":"Amaury","family":"Pouly","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Paris, IRIF, CNRS, France"}]},{"given":"James","family":"Worrell","sequence":"additional","affiliation":[{"name":"Oxford University, UK"}]}],"member":"320","published-online":{"date-parts":[[2023,10,11]]},"reference":[{"key":"e_1_3_2_2_2","volume-title":"Proceedings of the 45th International Colloquium on Automata, Languages and Programming","author":"Almagor S.","year":"2018","unstructured":"S. Almagor, D. Chistikov, J. Ouaknine, and J. Worrell. 2018. O-minimal invariants for linear loops. In Proceedings of the 45th International Colloquium on Automata, Languages and Programming. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_2_3_2","first-page":"498","volume-title":"Proceedings of the 7th Annual ACM-SIAM Symposium on Discrete Algorithms.","author":"Babai L.","year":"1996","unstructured":"L. Babai, R. Beals, J.-Y. Cai, G. Ivanyos, and E. M. Luks. 1996. Multiplicative equations over commuting matrices. In Proceedings of the 7th Annual ACM-SIAM Symposium on Discrete Algorithms.498\u2013507."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0913-3"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539703425861"},{"key":"e_1_3_2_6_2","volume-title":"The Calculus of Computation\u2014Decision Procedures with Applications to Verification","author":"Bradley A. R.","year":"2007","unstructured":"A. R. Bradley and Z. Manna. 2007. The Calculus of Computation\u2014Decision Procedures with Applications to Verification. Springer."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.02.028"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02945-9"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.004"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_12_2","volume-title":"Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra (2nd ed.)","author":"Cox D. A.","year":"1997","unstructured":"D. A. Cox, J. B. Little, and D. O\u2019Shea. 1997. Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra (2nd ed.). Springer-Verlag."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_30"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2004.11.008"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055044"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_9"},{"key":"e_1_3_2_17_2","first-page":"29:1\u201329:13","volume-title":"Proceedings of the 34th Symposium on Theoretical Aspects of Computer Science","author":"Fijalkow N.","year":"2017","unstructured":"N. Fijalkow, P. Ohlmann, J. Ouaknine, A. Pouly, and J. Worrell. 2017. Semialgebraic invariant synthesis for the Kannan-Lipton Orbit problem. In Proceedings of the 34th Symposium on Theoretical Aspects of Computer Science. 29:1\u201329:13."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-019-09913-3"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604138"},{"key":"e_1_3_2_20_2","volume-title":"Banach Center Publications (Differential Galois Theory)","author":"Hrushovski E.","year":"2002","unstructured":"E. Hrushovski. 2002. Computing the Galois group of a linear differential equation. In Banach Center Publications (Differential Galois Theory), Vol. 58. Institute of Mathematics, Polish Academy of Sciences."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_11"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90006-8"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/0021-8693(78)90249-1"},{"key":"e_1_3_2_24_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/978-3-642-37651-1_8","volume-title":"Programming Logics - Essays in Memory of Harald Ganzinger","author":"Kapur D.","year":"2013","unstructured":"D. Kapur. 2013. Elimination techniques for program analysis. In Programming Logics - Essays in Memory of Harald Ganzinger(Lecture Notes in Computer Science, Vol. 7797). 194\u2013215."},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_2_26_2","first-page":"54:1\u201354:33","article-title":"Non-linear reasoning for invariant synthesis","volume":"2","author":"Kincaid Z.","year":"2018","unstructured":"Z. Kincaid, J. Cyphert, J. Breck, and T. W. Reps. 2018. Non-linear reasoning for invariant synthesis. PACMPL 2, POPL (2018), 54:1\u201354:33.","journal-title":"PACMPL"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1006\/jcom.1999.0536"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_18"},{"key":"e_1_3_2_29_2","author":"Kovacs L.","year":"2018","unstructured":"L. Kovacs. 2018. personal communication.","journal-title":"personal communication"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2005.19"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90001-9"},{"issue":"6","key":"e_1_3_2_32_2","first-page":"539","article-title":"On certain insoluble problems concerning matrices","volume":"57","author":"Markov A.","year":"1947","unstructured":"A. Markov. 1947. On certain insoluble problems concerning matrices. Doklady Akad. Nauk SSSR 57, 6 (1947), 539\u2013542.","journal-title":"Doklady Akad. Nauk SSSR"},{"key":"e_1_3_2_33_2","volume-title":"New Advances in Transcendence Theory","author":"Masser D. W.","year":"1988","unstructured":"D. W. Masser. 1988. Linear relations on algebraic groups. In New Advances in Transcendence Theory. Cambridge University Press."},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2001.957836"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-018-0324-y"},{"key":"e_1_3_2_36_2","unstructured":"D. W. Morris. 2001. Introduction to Arithmetic Groups. arXiv:math\/0106063."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.05.004"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_85"},{"key":"e_1_3_2_39_2","first-page":"129","volume-title":"Proceedings of the International Symposium on Symbolic and Algebraic Computation","author":"Nosan Klara","year":"2022","unstructured":"Klara Nosan, Amaury Pouly, Sylvain Schmitz, Mahsa Shirmohammadi, and James Worrell. 2022. On the computation of the Zariski closure of finitely generated groups of matrices. In Proceedings of the International Symposium on Symbolic and Algebraic Computation. ACM, 129\u2013138."},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1142\/3767"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1002\/sapm1970491105"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611974782.12"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.003"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964028"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.06.003"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43932-7"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.2307\/j.ctvc77h7p"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3614319","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3614319","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:47Z","timestamp":1750178747000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3614319"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,11]]},"references-count":47,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2023,10,31]]}},"alternative-id":["10.1145\/3614319"],"URL":"https:\/\/doi.org\/10.1145\/3614319","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,11]]},"assertion":[{"value":"2023-04-08","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-07-17","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-10-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}