{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T06:08:08Z","timestamp":1780726088109,"version":"3.54.1"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2013,5,1]],"date-time":"2013-05-01T00:00:00Z","timestamp":1367366400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We describe a simple and efficient algorithm for proving the termination of a class of loops with nonlinear assignments to variables. The method is based on divergence testing for each variable in the cone-of-influence of the loop\u2019s condition. The analysis allows us to automatically prove the termination of loops that cannot be handled using previous techniques. We also describe a method for integrating our nonlinear termination proving technique into a larger termination proving framework that depends on linear reasoning.<\/jats:p>","DOI":"10.1007\/s00165-012-0252-5","type":"journal-article","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T07:53:07Z","timestamp":1340783587000},"page":"389-403","source":"Crossref","is-referenced-by-count":10,"title":["Proving termination of nonlinear command sequences"],"prefix":"10.1145","volume":"25","author":[{"given":"Domagoj","family":"Babi\u0107","sequence":"first","affiliation":[{"name":"Computer Science Division, University of California, Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Byron","family":"Cook","sequence":"additional","affiliation":[{"name":"Microsoft Research and University College London, London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alan J.","family":"Hu","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of British Columbia, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zvonimir","family":"Rakamari\u0107","sequence":"additional","affiliation":[{"name":"School of Computing, The University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Bouajjani A Bozga M Habermehl P Iosif R Moro P Vojnar T (2006) Programs with lists are counter automata. In: Proceedings of international conference on computer aided verification (CAV). pp 517\u2013531","DOI":"10.1007\/11817963_47"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Berdine J Chawdhary A Cook B Distefano D O\u2019Hearn P (2007) Variance analyses from invariance analyses. In: Proceedings of ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL). pp 211\u2013224","DOI":"10.1145\/1190215.1190249"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Babi\u0107 D Cook B Hu AJ Rakamari\u0107 Z (2007) Proving termination by divergence. In: Proceedings of IEEE international conference on software engineering and formal methods (SEFM). pp 93\u2013102","DOI":"10.1109\/SEFM.2007.32"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bradley A Manna Z Sipma H (2005) Termination of polynomial programs. In: Proceedings of international conference on verification model checking and abstract interpretation (VMCAI). pp 113\u2013129","DOI":"10.1007\/978-3-540-30579-8_8"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bradley AR Manna Z Sipma HB (2005) The polyranking principle. In: Proceedings of international colloquium on automata languages and programming (ICALP). pp 1349\u20131361","DOI":"10.1007\/11523468_109"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bradley AR Manna Z Sipma HB (2005) Termination analysis of integer linear loops. In: Proceedings of international conference on concurrency theory (CONCUR). pp 488\u2013502","DOI":"10.1007\/11539452_37"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Cousot P Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL). pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_2_1_2_9_2","unstructured":"Contejean E March\u00e9 C Monate B Urbain X (2003) Proving termination of rewriting with c i me. In: Extended abstracts of the sixth international workshop on termination (WST). pp 71\u201373"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Cousot P (2005) Proving program invariance and termination by parametric abstraction lagrangian relaxation and semidefinite programming. In: Proceedings of international conference on verification model checking and abstract interpretation (VMCAI). pp 1\u201324","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Cook B Podelski A Rybalchenko A (2005) Abstraction refinement for termination. In: Proceedings of international static analysis symposium (SAS). pp 87\u2013101","DOI":"10.1007\/11547662_8"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Cook B Podelski A Rybalchenko A (2006) Termination proofs for systems code. In: Proceedings of ACM SIGPLAN conference on programming language design and implementation (PLDI). pp 415\u2013426","DOI":"10.1145\/1133255.1134029"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Col\u00f3n M Sipma H (2002) Practical methods for proving program termination. In: Proceedings of international conference on computer aided verification (CAV). pp 442\u2013454","DOI":"10.1007\/3-540-45657-0_36"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(99)00006-0"},{"key":"e_1_2_1_2_15_2","volume-title":"Fixed point theory","author":"Dugundji J","year":"2003","edition":"1"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Robert W. Floyd (1967) Assigning meanings to programs. In: Mathematical Aspects of Computer Science vol 19 of Proceedings of Symposia in Applied Mathematics pages 19\u201332 American Mathematical Society","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Giesl J Thiemann R Schneider-Kamp P Falke S (2004) Automated termination proofs with AProVE. In: Proceedings of international conference on rewriting techniques and applications (RTA). pp 210\u2013220","DOI":"10.1007\/978-3-540-25979-4_15"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_19_2","unstructured":"Kaltofen E (1982) On the complexity of factoring polynomials with integer coefficients. PhD thesis Rensselaer Polytechnic Institute Troy NY USA"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01457454"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Lee CS Jones ND Ben-Amram AM (2001) The size-change principle for program termination. In: Proceedings of ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL). pp 81\u201392","DOI":"10.1145\/373243.360210"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Lindenstrauss N Sagiv Y Serebrenik A (1997) TermiLog. A system for checking termination of queries to logic programs. In: Proceedings of international conference on computer aided verification (CAV). pp 444\u2013447","DOI":"10.1007\/3-540-63166-6_44"},{"key":"e_1_2_1_2_23_2","unstructured":"Maplesoft (2004) Maple version 9.5"},{"key":"e_1_2_1_2_24_2","unstructured":"Magill S Berdine J Clarke E Cook B (2007) Arithmetic strengthening for shape analysis. In: Proceedings of international static analysis symposium (SAS)"},{"key":"e_1_2_1_2_25_2","unstructured":"Muchnick SS (1997) Advanced Compiler Design and Implementation. Morgan Kaufmann Publishers Inc. San Francisco"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Podelski A Rybalchenko A (2004) A complete method for the synthesis of linear ranking functions. In: Proceedings of international conference on verification model checking and abstract interpretation (VMCAI). pp 239\u2013251","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Chris Speirs Zoltan Somogyi Harald S\u00f8ndergaard (1997) Termination analysis for Mercury. In International Static Analysis Symposium (SAS) pages 160\u2013171","DOI":"10.1007\/BFb0032740"},{"key":"e_1_2_1_2_28_2","first-page":"121","article-title":"A survey of program slicing techniques","volume":"3","author":"Tip F.","year":"1995","journal-title":"Journal of programming languages"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Tiwari A (2004) Termination of linear programs. In: Proceedings of the international conference on computer aided verification (CAV). pp 70\u201382","DOI":"10.1007\/978-3-540-27813-9_6"},{"key":"e_1_2_1_2_30_2","unstructured":"Turing A (1949) Checking a large routine. In: Report of a conference on high speed automatic calculating machines. pp 67\u201369"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0252-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0252-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0252-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:53:37Z","timestamp":1641484417000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0252-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,5]]}},"alternative-id":["10.1007\/s00165-012-0252-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0252-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,5]]}}}