{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:23Z","timestamp":1772164043184,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,1,23]],"date-time":"2013-01-23T00:00:00Z","timestamp":1358899200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,1,23]]},"DOI":"10.1145\/2429069.2429078","type":"proceedings-article","created":{"date-parts":[[2013,1,22]],"date-time":"2013-01-22T10:29:29Z","timestamp":1358850569000},"page":"51-62","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["On the linear ranking problem for integer linear-constraint loops"],"prefix":"10.1145","author":[{"given":"Amir M.","family":"Ben-Amram","sequence":"first","affiliation":[{"name":"The Tel-Aviv Academic College, Tel Aviv, Israel"}]},{"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[{"name":"Complutense University of Madrid, Madrid, Spain"}]}],"member":"320","published-online":{"date-parts":[[2013,1,23]]},"reference":[{"key":"e_1_3_2_2_1_1","series-title":"LNCS","first-page":"113","volume-title":"Formal Methods for Components and Objects, FMCO'07","author":"Albert E.","year":"2007","unstructured":"E. Albert , P. Arenas , S. Genaim , G. Puebla , and D. Zanardini . Costa: Design and implementation of a cost and termination analyzer for java bytecode . In F. S. de Boer, M. M. Bonsangue, S. Graf, and W. P. de Roever, editors, Formal Methods for Components and Objects, FMCO'07 , volume 5382 of LNCS , pages 113 -- 132 . Springer , 2007 . E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Costa: Design and implementation of a cost and termination analyzer for java bytecode. In F. S. de Boer, M. M. Bonsangue, S. Graf, and W. P. de Roever, editors, Formal Methods for Components and Objects, FMCO'07, volume 5382 of LNCS, pages 113--132. Springer, 2007."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9174-1"},{"key":"e_1_3_2_2_3_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/978-3-642-15769-1_8","volume-title":"Static Analysis Symposium, SAS'10","author":"Alias C.","year":"2010","unstructured":"C. Alias , A. Darte , P. Feautrier , and L. Gonnord . Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs . In R. Cousot and M. Martel, editors, Static Analysis Symposium, SAS'10 , volume 6337 of LNCS , pages 117 -- 133 . Springer , 2010 . C. Alias, A. Darte, P. Feautrier, and L. Gonnord. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In R. Cousot and M. Martel, editors, Static Analysis Symposium, SAS'10, volume 6337 of LNCS, pages 117--133. Springer, 2010."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"crossref","unstructured":"R.\n      Bagnara P. M.\n      Hill and \n      E.\n      Zaffanella\n  . \n  An improved tight closure algorithm for integer octagonal constraints\n  . In F. Logozzo D. Peled and L. D. Zuck editors phVerification Model Checking and Abstract Interpretation VMCAI'08 volume \n  4905\n   of \n  LNCS pages \n  8\n  --\n  21\n  . \n  Springer 2008\n  .   R. Bagnara P. M. Hill and E. Zaffanella. An improved tight closure algorithm for integer octagonal constraints. In F. Logozzo D. Peled and L. D. Zuck editors phVerification Model Checking and Abstract Interpretation VMCAI'08 volume 4905 of LNCS pages 8--21. Springer 2008.","DOI":"10.1007\/978-3-540-78163-9_6"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.03.003"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1353445.1353450"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429078"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_6"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_18"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_7"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_37"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_109"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_8"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_34"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1216374.1216378"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02158-9_9"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562931_25"},{"key":"e_1_3_2_2_20_1","series-title":"LNCS","first-page":"67","volume-title":"T. Margaria and W. Yi","author":"Col\u00f3n M.","year":"2001","unstructured":"M. Col\u00f3n and H. Sipma . Synthesis of linear ranking functions . In T. Margaria and W. Yi , editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS'01, volume 2031 of LNCS , pages 67 -- 81 . Springer , 2001 . M. Col\u00f3n and H. Sipma. Synthesis of linear ranking functions. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS'01, volume 2031 of LNCS, pages 67--81. Springer, 2001."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_19"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"e_1_3_2_2_24_1","first-page":"139","volume-title":"MEMOCODE'10","author":"Darte A.","year":"2010","unstructured":"A. Darte . Understanding loops : The influence of the decomposition of Karp, Miller, and Winograd. In Formal Methods and Models for Codesign , MEMOCODE'10 , pages 139 -- 148 . IEEE Computer Society , 2010 . A. Darte. Understanding loops: The influence of the decomposition of Karp, Miller, and Winograd. In Formal Methods and Models for Codesign, MEMOCODE'10, pages 139--148. IEEE Computer Society, 2010."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01407835"},{"key":"e_1_3_2_2_26_1","volume-title":"Computers and Intractability","author":"Garey M. R.","year":"1979","unstructured":"M. R. Garey and D. S. Johnson . Computers and Intractability . W.H. Freeman and Co. , New York , 1979 . M. R. Garey and D. S. Johnson. Computers and Intractability. W.H. Freeman and Co., New York, 1979."},{"key":"e_1_3_2_2_27_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1007\/978-3-540-25979-4_15","volume-title":"Rewriting Techniques and Applications, RTA'04","author":"Giesl J.","year":"2004","unstructured":"J. Giesl , R. Thiemann , P. Schneider-Kamp , and S. Falke . Automated termination proofs with aprove . In V. van Oostrom, editor, Rewriting Techniques and Applications, RTA'04 , volume 3091 of LNCS , pages 210 -- 220 . Springer , 2004 . J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Automated termination proofs with aprove. In V. van Oostrom, editor, Rewriting Techniques and Applications, RTA'04, volume 3091 of LNCS, pages 210--220. Springer, 2004."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1137\/S009753979528977X"},{"key":"e_1_3_2_2_30_1","first-page":"102","volume-title":"Australasian Computer Science Conference, ACSC'97","author":"Harvey W.","year":"1997","unstructured":"W. Harvey and P. J. Stuckey . A unit two variable per inequality integer constraint solver for constraint logic programming . In Australasian Computer Science Conference, ACSC'97 , pages 102 -- 111 , 1997 . W. Harvey and P. J. Stuckey. A unit two variable per inequality integer constraint solver for constraint logic programming. In Australasian Computer Science Conference, ACSC'97, pages 102--111, 1997."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-2001-2_9"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1980.29"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/298514.298581"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_3_2_2_35_1","first-page":"64","volume-title":"International Conference on Logic Programming, ICLP'97","author":"Lindenstrauss N.","year":"1997","unstructured":"N. Lindenstrauss and Y. Sagiv . Automatic termination analysis of Prolog programs. In L. Naish, editor , International Conference on Logic Programming, ICLP'97 , pages 64 -- 77 . MIT Press , 1997 . N. Lindenstrauss and Y. Sagiv. Automatic termination analysis of Prolog programs. In L. Naish, editor, International Conference on Logic Programming, ICLP'97, pages 64--77. MIT Press, 1997."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068407003122"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"crossref","unstructured":"A.\n      Podelski\n     and \n      A.\n      Rybalchenko\n  . \n  A complete method for the synthesis of linear ranking functions\n  . In B. Steffen and G. Levi editors Verification Model Checking and Abstract Interpretation VMCAI'04 volume \n  2937\n   of \n  phLNCS pages \n  239\n  --\n  251\n  . \n  Springer 2004\n  .  A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In B. Steffen and G. Levi editors Verification Model Checking and Abstract Interpretation VMCAI'04 volume 2937 of phLNCS pages 239--251. Springer 2004.","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_3_2_2_39_1","volume-title":"SARA'09","author":"Revesz P. Z.","year":"2009","unstructured":"P. Z. Revesz . Tightened transitive closure of integer addition constraints. In V. Bulitko and J. C. Beck, editors, phSymposium on Abstraction, Reformulation, and Approximation , SARA'09 , 2009 . P. Z. Revesz. Tightened transitive closure of integer addition constraints. In V. Bulitko and J. C. Beck, editors, phSymposium on Abstraction, Reformulation, and Approximation, SARA'09, 2009."},{"key":"e_1_3_2_2_40_1","volume-title":"Universitat des Saarlandes","author":"Rybalchenko A.","year":"2004","unstructured":"A. Rybalchenko . phTemporal Verification with Transition Invariants. PhD thesis , Universitat des Saarlandes , 2004 . A. Rybalchenko. phTemporal Verification with Transition Invariants. PhD thesis, Universitat des Saarlandes, 2004."},{"key":"e_1_3_2_2_41_1","volume-title":"John Wiley and Sons","author":"Schrijver A.","year":"1986","unstructured":"A. Schrijver . Theory of Linear and Integer Programming . John Wiley and Sons , New York , 1986 . A. Schrijver. Theory of Linear and Integer Programming. John Wiley and Sons, New York, 1986."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/113413.113433"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709095"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1287\/opre.34.2.250"},{"key":"e_1_3_2_2_45_1","unstructured":"A.\n      Tiwari\n    .\n  Termination of linear programs\n  . In R. Alur and D. Peled editors Computer Aided\n   Verification CAV'04 volume \n  3114\n   of \n  LNCS pages \n  387\n  --\n  390\n  . \n  Springer 2004\n  .  A. Tiwari. Termination of linear programs. In R. Alur and D. Peled editors Computer Aided Verification CAV'04 volume 3114 of LNCS pages 387--390. Springer 2004."}],"event":{"name":"POPL '13: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Rome Italy","acronym":"POPL '13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2429069.2429078","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2429069.2429078","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:35Z","timestamp":1750221335000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2429069.2429078"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,23]]},"references-count":44,"alternative-id":["10.1145\/2429069.2429078","10.1145\/2429069"],"URL":"https:\/\/doi.org\/10.1145\/2429069.2429078","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2480359.2429078","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,1,23]]},"assertion":[{"value":"2013-01-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}