{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T22:10:34Z","timestamp":1769724634610,"version":"3.49.0"},"reference-count":49,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/501100004040","name":"KU Leuven","doi-asserted-by":"publisher","award":["iBOF\/23\/064"],"award-info":[{"award-number":["iBOF\/23\/064"]}],"id":[{"id":"10.13039\/501100004040","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004497","name":"KU Leuven Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004497","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003130","name":"Research Foundation Flanders","doi-asserted-by":"publisher","award":["G0F5921N"],"award-info":[{"award-number":["G0F5921N"]}],"id":[{"id":"10.13039\/501100003130","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Symbolic Computation"],"published-print":{"date-parts":[[2026,7]]},"DOI":"10.1016\/j.jsc.2025.102551","type":"journal-article","created":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T19:51:32Z","timestamp":1767210692000},"page":"102551","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Algebraic and algorithmic methods for computing polynomial loop invariants"],"prefix":"10.1016","volume":"135","author":[{"given":"Erdenebayar","family":"Bayarmagnai","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5187-0995","authenticated-orcid":false,"given":"Fatemeh","family":"Mohammadi","sequence":"additional","affiliation":[]},{"given":"R\u00e9mi","family":"Pr\u00e9bet","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.jsc.2025.102551_br0010","doi-asserted-by":"crossref","first-page":"745","DOI":"10.1145\/3704862","article-title":"Simple linear loops: algebraic invariants and applications","volume":"9, POPL","author":"Ait El Manssour","year":"2025","journal-title":"Proc. ACM Program. Lang."},{"key":"10.1016\/j.jsc.2025.102551_br0020","series-title":"International Static Analysis Symposium","first-page":"19","article-title":"Solving invariant generation for unsolvable loops","author":"Amrollahi","year":"2022"},{"issue":"1","key":"10.1016\/j.jsc.2025.102551_br0030","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/s10703-024-00455-0","article-title":"(Un) solvable loop analysis","volume":"65","author":"Amrollahi","year":"2025","journal-title":"Form. Methods Syst. Des."},{"key":"10.1016\/j.jsc.2025.102551_br0040","series-title":"Algorithms in Real Algebraic Geometry","author":"Basu","year":"2006"},{"key":"10.1016\/j.jsc.2025.102551_br0050","series-title":"Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation","first-page":"371","article-title":"Algebraic tools for computing polynomial loop invariants","author":"Bayarmagnai","year":"2024"},{"key":"10.1016\/j.jsc.2025.102551_br0490","series-title":"Proceedings of the 14th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis","first-page":"1","article-title":"Beyond affine loops: A geometric approach to program synthesis","author":"Bayarmagnai","year":"2025"},{"key":"10.1016\/j.jsc.2025.102551_br0060","series-title":"2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science","first-page":"1","article-title":"Polynomial automata: zeroness and applications","author":"Benedikt","year":"2017"},{"key":"10.1016\/j.jsc.2025.102551_br0070","series-title":"Proceedings of the 2021 on International Symposium on Symbolic and Algebraic Computation","first-page":"51","article-title":"Msolve: a library for solving polynomial systems","author":"Berthomieu","year":"2021"},{"key":"10.1016\/j.jsc.2025.102551_br0080","article-title":"Real Algebraic Geometry","volume":"vol. 3","author":"Bochnack","year":"1998"},{"key":"10.1016\/j.jsc.2025.102551_br0090","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.scico.2014.02.028","article-title":"Inference of polynomial invariants for imperative programs: a farewell to Gr\u00f6bner bases","volume":"93","author":"Cachera","year":"2014","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.jsc.2025.102551_br0100","series-title":"Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation","first-page":"672","article-title":"Polynomial invariant generation for non-deterministic recursive programs","author":"Chatterjee","year":"2020"},{"key":"10.1016\/j.jsc.2025.102551_br0110","series-title":"Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra","author":"Cox","year":"2013"},{"key":"10.1016\/j.jsc.2025.102551_br0120","doi-asserted-by":"crossref","first-page":"724","DOI":"10.1145\/3632867","article-title":"Solvable polynomial ideals: the ideal reflection for program analysis","volume":"8, POPL","author":"Cyphert","year":"2024","journal-title":"Proc. ACM Program. Lang."},{"key":"10.1016\/j.jsc.2025.102551_br0130","series-title":"Automated Technology for Verification and Analysis: 14th International Symposium","first-page":"479","article-title":"Polynomial invariants by linear algebra","author":"de Oliveira","year":"2016"},{"key":"10.1016\/j.jsc.2025.102551_br0140","series-title":"International Symposium on Automated Technology for Verification and Analysis","first-page":"327","article-title":"Synthesizing invariants by solving solvable loops","author":"de Oliveira","year":"2017"},{"key":"10.1016\/j.jsc.2025.102551_br0150","doi-asserted-by":"crossref","first-page":"719","DOI":"10.1016\/j.jsc.2016.07.031","article-title":"A survey on signature-based algorithms for computing Gr\u00f6bner bases","volume":"80","author":"Eder","year":"2017","journal-title":"J. Symb. Comput."},{"key":"10.1016\/j.jsc.2025.102551_br0160","series-title":"Program Verification: Fundamental Issues in Computer Science","first-page":"65","article-title":"Assigning meanings to programs","author":"Floyd","year":"1993"},{"key":"10.1016\/j.jsc.2025.102551_br0170","doi-asserted-by":"crossref","first-page":"727","DOI":"10.1145\/3586052","article-title":"Algebro-geometric algorithms for template-based synthesis of polynomial programs","volume":"7, OOPSLA1","author":"Goharshady","year":"2023","journal-title":"Proc. ACM Program. Lang."},{"key":"10.1016\/j.jsc.2025.102551_br0180","series-title":"Macaulay2, a software system for research in algebraic geometry","author":"Grayson","year":"2002"},{"key":"10.1016\/j.jsc.2025.102551_br0190","series-title":"Algebraic Geometry, vol. 52","author":"Hartshorne","year":"2013"},{"key":"10.1016\/j.jsc.2025.102551_br0200","series-title":"Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science","first-page":"530","article-title":"Polynomial invariants for affine programs","author":"Hrushovski","year":"2018"},{"issue":"5","key":"10.1016\/j.jsc.2025.102551_br0210","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3614319","article-title":"On strongest algebraic program invariants","volume":"70","author":"Hrushovski","year":"2023","journal-title":"J. ACM"},{"key":"10.1016\/j.jsc.2025.102551_br0220","series-title":"International Conference on Verification, Model Checking, and Abstract Interpretation","first-page":"226","article-title":"Invariant generation for multi-path loops with polynomial assignments","author":"Humenberger","year":"2017"},{"key":"10.1016\/j.jsc.2025.102551_br0230","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/BF00268497","article-title":"Affine relationships among variables of a program","volume":"6","author":"Karr","year":"1976","journal-title":"Acta Inform."},{"issue":"4","key":"10.1016\/j.jsc.2025.102551_br0240","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1145\/360032.360048","article-title":"Logical analysis of programs","volume":"19","author":"Katz","year":"1976","journal-title":"Commun. ACM"},{"key":"10.1016\/j.jsc.2025.102551_br0250","series-title":"Algebraic Varieties","author":"Kempf","year":"1993"},{"issue":"4","key":"10.1016\/j.jsc.2025.102551_br0260","doi-asserted-by":"crossref","first-page":"963","DOI":"10.1090\/S0894-0347-1988-0944576-7","article-title":"Sharp effective nullstellensatz","volume":"1","author":"Koll\u00e1r","year":"1988","journal-title":"J. Am. Math. Soc."},{"key":"10.1016\/j.jsc.2025.102551_br0270","series-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"249","article-title":"Reasoning algebraically about p-solvable loops","author":"Kov\u00e1cs","year":"2008"},{"key":"10.1016\/j.jsc.2025.102551_br0280","series-title":"Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation","first-page":"41","article-title":"Algebra-based loop analysis","author":"Kov\u00e1cs","year":"2023"},{"key":"10.1016\/j.jsc.2025.102551_br0290","series-title":"Temporal Verification of Reactive Systems: Safety","author":"Manna","year":"2012"},{"key":"10.1016\/j.jsc.2025.102551_br0300","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/0001-8708(82)90048-2","article-title":"The complexity of the word problem for commutative semi-groups and polynomial ideals","volume":"46","author":"Mayr","year":"1982","journal-title":"Adv. Math."},{"key":"10.1016\/j.jsc.2025.102551_br0310","doi-asserted-by":"crossref","first-page":"1497","DOI":"10.1145\/3563341","article-title":"This is the moment for probabilistic loops","volume":"6, OOPSLA2","author":"Moosbrugger","year":"2022","journal-title":"Proc. ACM Program. Lang."},{"key":"10.1016\/j.jsc.2025.102551_br0320","doi-asserted-by":"crossref","first-page":"181","DOI":"10.7146\/math.scand.a-12421","article-title":"Length of polynomial ascending chains and primitive recursiveness","volume":"71","author":"Moreno Socias","year":"1992","journal-title":"Math. Scand."},{"issue":"5","key":"10.1016\/j.jsc.2025.102551_br0330","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1016\/j.ipl.2004.05.004","article-title":"Computing polynomial program invariants","volume":"91","author":"M\u00fcller-Olm","year":"2004","journal-title":"Inf. Process. Lett."},{"key":"10.1016\/j.jsc.2025.102551_br0340","series-title":"International Colloquium on Automata, Languages, and Programming","first-page":"1016","article-title":"A note on Karr's algorithm","author":"M\u00fcller-Olm","year":"2004"},{"key":"10.1016\/j.jsc.2025.102551_br0350","article-title":"Strong invariants are hard: on the hardness of strongest polynomial invariants for (probabilistic) programs","volume":"8, POPL","author":"M\u00fcllner","year":"2024","journal-title":"Proc. ACM Program. Lang."},{"key":"10.1016\/j.jsc.2025.102551_br0360","series-title":"Proceedings of the 2022 International Symposium on Symbolic and Algebraic Computation (Villeneuve-d'Ascq, France)","first-page":"129","article-title":"On the computation of the Zariski closure of finitely generated groups of matrices","author":"Nosan","year":"2022"},{"issue":"2","key":"10.1016\/j.jsc.2025.102551_br0370","doi-asserted-by":"crossref","first-page":"563","DOI":"10.5802\/aif.1683","article-title":"Trajectories of polynomial vector fields and ascending chains of polynomial ideals","volume":"49","author":"Novikov","year":"1999","journal-title":"Ann. Inst. Fourier"},{"issue":"6","key":"10.1016\/j.jsc.2025.102551_br0380","doi-asserted-by":"crossref","first-page":"2652","DOI":"10.3906\/mat-1904-61","article-title":"Ascending chains of ideals in the polynomial ring","volume":"44","author":"Pastuszak","year":"2020","journal-title":"Turk. J. Math."},{"issue":"3","key":"10.1016\/j.jsc.2025.102551_br0390","doi-asserted-by":"crossref","first-page":"969","DOI":"10.1512\/iumj.1993.42.42045","article-title":"Positive polynomials on compact semi-algebraic sets","volume":"42","author":"Putinar","year":"1993","journal-title":"Indiana Univ. Math. J."},{"key":"10.1016\/j.jsc.2025.102551_br0400","series-title":"Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation","first-page":"266","article-title":"Automatic generation of polynomial loop invariants: algebraic foundations","author":"Rodr\u00edguez-Carbonell","year":"2004"},{"issue":"1","key":"10.1016\/j.jsc.2025.102551_br0410","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1016\/j.scico.2006.03.003","article-title":"Automatic generation of polynomial invariants of bounded degree using abstract interpretation","volume":"64","author":"Rodr\u00edguez-Carbonell","year":"2007","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"10.1016\/j.jsc.2025.102551_br0420","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1016\/j.jsc.2007.01.002","article-title":"Generating all polynomial invariants in simple loops","volume":"42","author":"Rodr\u00edguez-Carbonell","year":"2007","journal-title":"J. Symb. Comput."},{"key":"10.1016\/j.jsc.2025.102551_br0430","series-title":"Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","first-page":"318","article-title":"Non-linear loop invariant generation using Gr\u00f6bner bases","author":"Sankaranarayanan","year":"2004"},{"key":"10.1016\/j.jsc.2025.102551_br0440","first-page":"305","article-title":"Constructive proof of Hilbert's theorem on ascending chains","volume":"174","author":"Seidenberg","year":"1972","journal-title":"Trans. Am. Math. Soc."},{"issue":"4","key":"10.1016\/j.jsc.2025.102551_br0450","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1016\/S0747-7171(08)80104-6","article-title":"An algorithm for solving parametric linear systems","volume":"13","author":"Sit","year":"1992","journal-title":"J. Symb. Comput."},{"key":"10.1016\/j.jsc.2025.102551_br0460","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.jsc.2012.06.004","article-title":"On the bit-complexity of sparse polynomial and series multiplication","volume":"50","author":"van der Hoeven","year":"2013","journal-title":"J. Symb. Comput."},{"key":"10.1016\/j.jsc.2025.102551_br0470","series-title":"Modern Computer Algebra","author":"Zur Gathen","year":"2013"},{"key":"10.1016\/j.jsc.2025.102551_br0480","series-title":"Computer Aided Verification, Arie Gurfinkel","first-page":"409","article-title":"On polynomial expressions with C-finite recurrences in loops with nested nondeterministic branches","author":"Wang","year":"2024"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717125001336?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717125001336?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,1,28]],"date-time":"2026-01-28T12:42:44Z","timestamp":1769604164000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717125001336"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7]]},"references-count":49,"alternative-id":["S0747717125001336"],"URL":"https:\/\/doi.org\/10.1016\/j.jsc.2025.102551","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[2026,7]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Algebraic and algorithmic methods for computing polynomial loop invariants","name":"articletitle","label":"Article Title"},{"value":"Journal of Symbolic Computation","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jsc.2025.102551","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2025 Elsevier Ltd. All rights are reserved, including those for text and data mining, AI training, and similar technologies.","name":"copyright","label":"Copyright"}],"article-number":"102551"}}