{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:25:05Z","timestamp":1750307105669,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2012,12,1]],"date-time":"2012-12-01T00:00:00Z","timestamp":1354320000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"GPD Research Group","award":["UCM-BSCH-GR35\/10-A-910502"],"award-info":[{"award-number":["UCM-BSCH-GR35\/10-A-910502"]}]},{"name":"PROMETIDOS-CM project","award":["S2009TIC-1465"],"award-info":[{"award-number":["S2009TIC-1465"]}]},{"name":"DOVES project","award":["TIN-2008-05624"],"award-info":[{"award-number":["TIN-2008-05624"]}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["ICT-231620"],"award-info":[{"award-number":["ICT-231620"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2012,12]]},"abstract":"<jats:p>\n            In this article we study the decidability of termination of several variants of simple integer loops, without branching in the loop body and with affine constraints as the loop guard (and possibly a precondition). We show that termination of such loops is undecidable in some cases, in particular, when the body of the loop is expressed by a set of linear inequalities where the coefficients are from Z \u222a {\n            <jats:italic>r<\/jats:italic>\n            } with\n            <jats:italic>r<\/jats:italic>\n            an arbitrary irrational; when the loop is a sequence of instructions, that compute either linear expressions or the step function; and when the loop body is a piecewise linear deterministic update with two pieces. The undecidability result is proven by a reduction from counter programs, whose termination is known to be undecidable. For the common case of integer linear-constraint loops with rational coefficients we have not succeeded in proving either decidability or undecidability of termination, but we show that a Petri net can be simulated with such a loop; this implies some interesting lower bounds. For example, termination for a partially specified input is at least EXPSPACE-hard.\n          <\/jats:p>","DOI":"10.1145\/2400676.2400679","type":"journal-article","created":{"date-parts":[[2013,1,11]],"date-time":"2013-01-11T15:42:48Z","timestamp":1357918968000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["On the Termination of Integer Loops"],"prefix":"10.1145","volume":"34","author":[{"given":"Amir M.","family":"Ben-Amram","sequence":"first","affiliation":[{"name":"The Academic College of Tel-Aviv Yaffo"}]},{"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[{"name":"Complutense University of Madrid"}]},{"given":"Abu Naser","family":"Masud","sequence":"additional","affiliation":[{"name":"Technical University of Madrid"}]}],"member":"320","published-online":{"date-parts":[[2012,12]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO\u201907)","volume":"5382","author":"Albert E.","unstructured":"Albert , E. , Arenas , P. , Genaim , S. , Puebla , G. , and Zanardini , D . 2007. Costa: Design and implementation of a cost and termination analyzer for java bytecode . In Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO\u201907) . F. S. de Boer, M. M. Bonsangue, S. Graf, and W. P. de Roever Eds., Lecture Notes in Computer Science , vol. 5382 , Springer, 113--132. Albert, E., Arenas, P., Genaim, S., Puebla, G., and Zanardini, D. 2007. Costa: Design and implementation of a cost and termination analyzer for java bytecode. In Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO\u201907). F. S. de Boer, M. M. Bonsangue, S. Graf, and W. P. de Roever Eds., Lecture Notes in Computer Science, vol. 5382, Springer, 113--132."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.03.003"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1353445.1353450"},{"key":"e_1_2_1_4_1","first-page":"3","article-title":"Size-Change termination, monotonicity constraints and ranking functions","volume":"6","author":"Ben-Amram A. M.","year":"2010","unstructured":"Ben-Amram , A. M. 2010 . Size-Change termination, monotonicity constraints and ranking functions . Logic. Meth. Comput. Sci. 6 , 3 . Ben-Amram, A. M. 2010. Size-Change termination, monotonicity constraints and ranking functions. Logic. Meth. Comput. Sci. 6, 3.","journal-title":"Logic. Meth. Comput. Sci."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(3:4)2011"},{"key":"e_1_2_1_6_1","unstructured":"Ben-Amram A. M.\n     and \n      Codish M\n  . \n  2008\n  . A SAT-based approach to size change termination with global ranking functions. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908). C. Ramakrishnan and J. Rehof Eds. Lecture Notes in Computer Science vol. \n  5028 Springer 46--55. Ben-Amram A. M. and Codish M. 2008. A SAT-based approach to size change termination with global ranking functions. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908) . C. Ramakrishnan and J. Rehof Eds. Lecture Notes in Computer Science vol. 5028 Springer 46--55."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180475.1180480"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_6"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00399-6"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_18"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_7"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_37"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_34"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1216374.1216378"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562931_25"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Col\u00f3n M.\n     and \n      Sipma H\n  . \n  2001\n  . Synthesis of linear ranking functions. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901). T. Margaria and W. Yi Eds. Lecture Notes in Computer Science vol. \n  2031 Springer 67--81. Col\u00f3n M. and Sipma H. 2001. Synthesis of linear ranking functions. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901) . T. Margaria and W. Yi Eds. Lecture Notes in Computer Science vol. 2031 Springer 67--81.","DOI":"10.1007\/3-540-45319-9_6"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Dufourd C. Jancar P. and \n      Schnoebelen P\n  . \n  1999\n  . Boundedness of reset p\/t nets. In Proceedings of the International Colloquium on Automata Languages and Programming (ICALP\u201999). J. Wiedermann P. van Emde Boas and M. Nielsen Eds. Lecture Notes in Computer Science vol. \n  1644 Springer 301--310. Dufourd C. Jancar P. and Schnoebelen P. 1999. Boundedness of reset p\/t nets. In Proceedings of the International Colloquium on Automata Languages and Programming (ICALP\u201999) . J. Wiedermann P. van Emde Boas and M. Nielsen Eds. Lecture Notes in Computer Science vol. 1644 Springer 301--310.","DOI":"10.1007\/3-540-48523-6_27"},{"key":"e_1_2_1_19_1","series-title":"Lectures on Petri NetsLecture Notes in Computer Science","volume-title":"Decidability and complexity of Petri net problems -- An introduction","author":"Esparza J.","unstructured":"Esparza , J. 1998. Decidability and complexity of Petri net problems -- An introduction . In Lectures on Petri Nets , Vol. I : Basic Models. W. Reisig and G. Rozenberg Eds., Lecture Notes in Computer Science , vol. 1491, Springer , 374--428. Esparza, J. 1998. Decidability and complexity of Petri net problems -- An introduction. In Lectures on Petri Nets, Vol. I: Basic Models. W. Reisig and G. Rozenberg Eds., Lecture Notes in Computer Science, vol. 1491, Springer, 374--428."},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Esparza J. and Nielsen M. 1994. Decidability issues for Petri nets. Tech. rep. RS-94-8 BRICS Department of Computer Science University of Aarhus. Esparza J. and Nielsen M. 1994. Decidability issues for Petri nets. Tech. rep. RS-94-8 BRICS Department of Computer Science University of Aarhus.","DOI":"10.7146\/brics.v1i8.21662"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Giesl J. Thiemann R. Schneider-Kamp P. and \n      Falke S\n  . \n  2004\n  . Automated termination proofs with aprove. In Proceedings of the International Conference on Rewriting Techniques and Applications (RTA\u201904). V. van Oostrom Ed. Lecture Notes in Computer Science vol. \n  3091 Springer 210--220. Giesl J. Thiemann R. Schneider-Kamp P. and Falke S. 2004. Automated termination proofs with aprove. In Proceedings of the International Conference on Rewriting Techniques and Applications (RTA\u201904) . V. van Oostrom Ed. Lecture Notes in Computer Science vol. 3091 Springer 210--220.","DOI":"10.1007\/978-3-540-25979-4_15"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890030"},{"volume-title":"Decidability questions for Petri nets. Tech. rep. MIT\/LCS\/TR-161","author":"Hack M.","key":"e_1_2_1_23_1","unstructured":"Hack , M. 1976. Decidability questions for Petri nets. Tech. rep. MIT\/LCS\/TR-161 , Massachusetts Institute of Technology . Hack, M. 1976. Decidability questions for Petri nets. Tech. rep. MIT\/LCS\/TR-161, Massachusetts Institute of Technology."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00037-W"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Kurtz S. A.\n     and \n      Simon J\n  . \n  2007\n  . The undecidability of the generalized Collatz problem. In Proceedings of the Annual Conference on Theory and Applications of Models of Computation (TAMC\u201907). J.-Y. Cai S. B. Cooper and H. Zhu Eds. Lecture Notes in Computer Science vol. \n  4484 Springer 542--553. Kurtz S. A. and Simon J. 2007. The undecidability of the generalized Collatz problem. In Proceedings of the Annual Conference on Theory and Applications of Models of Computation (TAMC\u201907) . J.-Y. Cai S. B. Cooper and H. Zhu Eds. Lecture Notes in Computer Science vol. 4484 Springer 542--553.","DOI":"10.1007\/978-3-540-72504-6_49"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"volume-title":"Proceedings of the International Conference on Logic Programming (ICLP\u201997)","author":"Lindenstrauss N.","key":"e_1_2_1_27_1","unstructured":"Lindenstrauss , N. and Sagiv , Y . 1997. Automatic termination analysis of Prolog programs . In Proceedings of the International Conference on Logic Programming (ICLP\u201997) . L. Naish Ed., MIT Press, 64--77. Lindenstrauss, N. and Sagiv, Y. 1997. Automatic termination analysis of Prolog programs. In Proceedings of the International Conference on Logic Programming (ICLP\u201997). L. Naish Ed., MIT Press, 64--77."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.736024"},{"volume-title":"The reachability problem requires exponential space. Tech. rep. 63","author":"Lipton R. J.","key":"e_1_2_1_29_1","unstructured":"Lipton , R. J. 1976. The reachability problem requires exponential space. Tech. rep. 63 , Yale University . Lipton, R. J. 1976. The reachability problem requires exponential space. Tech. rep. 63, Yale University."},{"volume-title":"Hilbert\u2019s Tenth Problem: Relations with Arithmetic and Algebraic Geometry (AMS\u201900)","author":"Matiyasevich 0.","key":"e_1_2_1_30_1","unstructured":"Matiyasevich . 200 0. Hilbert\u2019s tenth problem: What was done and what is to be done . In Hilbert\u2019s Tenth Problem: Relations with Arithmetic and Algebraic Geometry (AMS\u201900) . J. Denef, L. Lipshitz, T. Pheidas, and V. Geel Eds., American Mathematical Society . Matiyasevich. 2000. Hilbert\u2019s tenth problem: What was done and what is to be done. In Hilbert\u2019s Tenth Problem: Relations with Arithmetic and Algebraic Geometry (AMS\u201900). J. Denef, L. Lipshitz, T. Pheidas, and V. Geel Eds., American Mathematical Society."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-6280-4_16"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Memmi G.\n     and \n      Roucairol G\n  . \n  1980\n  . Linear algebra in net theory. In Net Theory and Applications W. Brauer Ed. Lecture Notes in Computer Science vol. \n  84 Springer 213--223. Memmi G. and Roucairol G. 1980. Linear algebra in net theory. In Net Theory and Applications W. Brauer Ed. Lecture Notes in Computer Science vol. 84 Springer 213--223.","DOI":"10.1007\/3-540-10001-6_24"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068407003122"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01262932"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Podelski A.\n     and \n      Rybalchenko A\n  . \n  2004\n  . A complete method for the synthesis of linear ranking functions. In Proceedings of the International Conference on Verification Model Checking and Abstract Interpretation (VMCAI\u201904). B. Steffen and G. Levi Eds. Lecture Notes in Computer Science vol. \n  2937 Springer 239--251. Podelski A. and Rybalchenko A. 2004. A complete method for the synthesis of linear ranking functions. In Proceedings of the International Conference on Verification Model Checking and Abstract Interpretation (VMCAI\u201904) . B. Steffen and G. Levi Eds. Lecture Notes in Computer Science vol. 2937 Springer 239--251.","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/3405"},{"volume-title":"Recursion Theory","author":"Shoenfield J. R.","key":"e_1_2_1_39_1","unstructured":"Shoenfield , J. R. 1993. Recursion Theory . Springer . Shoenfield, J. R. 1993. Recursion Theory. Springer."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/113413.113433"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709095"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_6"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2400676.2400679","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2400676.2400679","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:35:01Z","timestamp":1750239301000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2400676.2400679"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,12]]},"references-count":42,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,12]]}},"alternative-id":["10.1145\/2400676.2400679"],"URL":"https:\/\/doi.org\/10.1145\/2400676.2400679","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2012,12]]},"assertion":[{"value":"2012-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-12-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}