{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T04:26:37Z","timestamp":1743135997392,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642279393"},{"type":"electronic","value":"9783642279409"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-27940-9_6","type":"book-chapter","created":{"date-parts":[[2012,1,19]],"date-time":"2012-01-19T02:29:29Z","timestamp":1326940169000},"page":"72-87","source":"Crossref","is-referenced-by-count":7,"title":["On the Termination of Integer Loops"],"prefix":"10.1007","author":[{"given":"Amir M.","family":"Ben-Amram","sequence":"first","affiliation":[]},{"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[]},{"given":"Abu Naser","family":"Masud","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-92188-2_5","volume-title":"Formal Methods for Components and Objects","author":"E. Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol.\u00a05382, pp. 113\u2013132. Springer, Heidelberg (2008)"},{"key":"6_CR2","unstructured":"Bagnara, R., Mesnard, F., Pescetti, A., Zaffanella, E.: The automatic synthesis of linear ranking functions: The complete unabridged version. Quaderno 498, Dipartimento di Matematica, Universit\u00e0 di Parma, Italy, Published as arXiv:cs.PL\/1004.0944 (2010)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M.: Size-change termination with difference constraints. ACM Trans. Program. Lang. Syst.\u00a030(3) (2008)","DOI":"10.1145\/1353445.1353450"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M.: Size-change termination, monotonicity constraints and ranking functions. Logical Methods in Computer Science\u00a06(3) (2010)","DOI":"10.2168\/LMCS-6(3:2)2010"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M.: Monotonicity constraints for termination in the integer domain. CoRR, abs\/1105.6317 (2011)","DOI":"10.2168\/LMCS-7(3:4)2011"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Lee, C.S.: Program termination analysis in polynomial time. ACM Trans. Program. Lang. Syst.\u00a029(1) (2007)","DOI":"10.1145\/1180475.1180480"},{"issue":"1-2","key":"6_CR7","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1016\/S0304-3975(00)00399-6","volume":"255","author":"V.D. Blondel","year":"2001","unstructured":"Blondel, V.D., Bournez, O., Koiran, P., Papadimitriou, C.H., Tsitsiklis, J.N.: Deciding stability and mortality of piecewise affine dynamical systems. Theor. Comput. Sci.\u00a0255(1-2), 687\u2013696 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR8","series-title":"LNCS","first-page":"88","volume-title":"VMCAI 2012","author":"L. Bozzelli","year":"2012","unstructured":"Bozzelli, L., Pinchinat, S.: Verification of Gap-Order Constraint Abstractions of Counter Systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 88\u2013103. Springer, Heidelberg (2012)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/11539452_37","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Termination Analysis of Integer Linear Loops. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 488\u2013502. Springer, Heidelberg (2005)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/11817963_34","volume-title":"Computer Aided Verification","author":"M. Braverman","year":"2006","unstructured":"Braverman, M.: Termination of Integer Linear Programs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 372\u2013385. Springer, Heidelberg (2006)"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Bruynooghe, M., Codish, M., Gallagher, J.P., Genaim, S., Vanhoof, W.: Termination analysis of logic programs through combination of type-based norms. ACM Trans. Program. Lang. Syst.\u00a029(2) (2007)","DOI":"10.1145\/1216374.1216378"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Schwartzbach, M.I., Ball, T. (eds.) Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation (PLDI), Ottawa, Canada, pp. 415\u2013426. ACM (2006); Terminator","DOI":"10.1145\/1133981.1134029"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/3-540-48523-6_27","volume-title":"Automata, Languages and Programming","author":"C. Dufourd","year":"1999","unstructured":"Dufourd, C., Jan\u010dar, P., Schnoebelen, P.: Boundedness of Reset P\/T Nets. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol.\u00a01644, pp. 301\u2013310. Springer, Heidelberg (1999)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/3-540-65306-6_20","volume-title":"Lectures on Petri Nets I: Basic Models","author":"J. Esparza","year":"1998","unstructured":"Esparza, J.: Decidability and Complexity of Petri Net Problems\u2014an Introduction. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol.\u00a01491, pp. 374\u2013428. Springer, Heidelberg (1998)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-540-25979-4_15","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"2004","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated Termination Proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 210\u2013220. Springer, Heidelberg (2004)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL, pp. 81\u201392 (2001)","DOI":"10.1145\/373243.360210"},{"key":"6_CR17","unstructured":"Lipton, R.J.: The reachability problem requires exponential space. Technical Report\u00a063, Yale University (1976), \n                  \n                    http:\/\/www.cs.yale.edu\/publications\/techreports\/tr63.pdf"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Matiyasevich, Y.: Hilbert\u2019s tenth problem: What was done and what is to be done. In: Denef, J., Lipshitz, L., Pheidas, T., Van Geel, J. (eds.) Hilbert\u2019s Tenth Problem: Relations with Arithmetic and Algebraic Geometry. AMS (2000)","DOI":"10.1090\/conm\/270\/04368"},{"issue":"1","key":"6_CR19","first-page":"111","volume":"8","author":"F. Mesnard","year":"2008","unstructured":"Mesnard, F., Serebrenik, A.: Recurrence with affine level mappings is p-time decidable for clp(r). TPLP\u00a08(1), 111\u2013119 (2008)","journal-title":"TPLP"},{"key":"6_CR20","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BF01262932","volume":"16","author":"R.R. Meyer","year":"1975","unstructured":"Meyer, R.R.: Integer and mixed-integer programming models: General properties. Journal of Optimization Theory and Applications\u00a016, 191\u2013206 (1975), doi:10.1007\/BF01262932","journal-title":"Journal of Optimization Theory and Applications"},{"key":"6_CR21","volume-title":"Computation: finite and infinite machines","author":"M.L. Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall, Inc., Upper Saddle River (1967)"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A Complete Method for the Synthesis of Linear Ranking Functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"6_CR23","series-title":"EATCS Monographs on Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69968-9","volume-title":"Petri Nets: An Introduction","author":"W. Reisig","year":"1985","unstructured":"Reisig, W.: Petri Nets: An Introduction. EATCS Monographs on Theoretical Computer Science. Springer, Berlin (1985)"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Sohn, K., Van Gelder, A.: Termination detection in logic programs using argument sizes. In: PODS, pp. 216\u2013226. ACM Press (1991)","DOI":"10.1145\/113413.113433"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Spoto, F., Mesnard, F., Payet, \u00c9.: A termination analyzer for java bytecode based on path-length. ACM Trans. Program. Lang. Syst.\u00a032(3) (2010)","DOI":"10.1145\/1709093.1709095"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-27813-9_6","volume-title":"Computer Aided Verification","author":"A. Tiwari","year":"2004","unstructured":"Tiwari, A.: Termination of Linear Programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 70\u201382. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27940-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,24]],"date-time":"2019-04-24T22:51:41Z","timestamp":1556146301000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27940-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642279393","9783642279409"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27940-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}