{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:30:25Z","timestamp":1759638625520,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,9,16]],"date-time":"2013-09-16T00:00:00Z","timestamp":1379289600000},"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,9,16]]},"DOI":"10.1145\/2505879.2505884","type":"proceedings-article","created":{"date-parts":[[2013,9,17]],"date-time":"2013-09-17T19:57:05Z","timestamp":1379447825000},"page":"229-238","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Eventual linear ranking functions"],"prefix":"10.1145","author":[{"given":"Roberto","family":"Bagnara","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Parma, Italy"}]},{"given":"Fred","family":"Mesnard","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de la R\u00e9union, France"}]}],"member":"320","published-online":{"date-parts":[[2013,9,16]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_1_1_1","DOI":"10.1016\/j.entcs.2009.12.008"},{"key":"e_1_3_2_1_2_1","volume-title":"Aix-en-Provence","author":"Alezan A.","year":"2013","unstructured":"A. Alezan , R. Bagnara , F. Mesnard , and E. Payet . D\u00e9tection des fonctions de rang lin\u00e9aires \u00e0 terme. In Actes des Neuvi\u00c3\u013ames Journ\u00c3l'es Francophones de Programmation par Contraintes (JFPC 2013), pages 11--20 , Aix-en-Provence , France , 2013 . In French. A. Alezan, R. Bagnara, F. Mesnard, and E. Payet. D\u00e9tection des fonctions de rang lin\u00e9aires \u00e0 terme. In Actes des Neuvi\u00c3\u013ames Journ\u00c3l'es Francophones de Programmation par Contraintes (JFPC 2013), pages 11--20, Aix-en-Provence, France, 2013. In French."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1109\/ICST.2013.17"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_4_1","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_3_2_1_5_1","volume-title":"The automatic synthesis of linear ranking functions: The complete unabridged version. Report arXiv:cs.PL\/1004.0944v2","author":"Bagnara R.","year":"2012","unstructured":"R. Bagnara , F. Mesnard , A. Pescetti , and E. Zaffanella . The automatic synthesis of linear ranking functions: The complete unabridged version. Report arXiv:cs.PL\/1004.0944v2 , 2012 . Available at http:\/\/arxiv.org\/ and http:\/\/bugseng.com\/products\/ppl\/. R. Bagnara, F. Mesnard, A. Pescetti, and E. Zaffanella. The automatic synthesis of linear ranking functions: The complete unabridged version. Report arXiv:cs.PL\/1004.0944v2, 2012. Available at http:\/\/arxiv.org\/ and http:\/\/bugseng.com\/products\/ppl\/."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.1016\/j.ic.2012.03.003"},{"key":"e_1_3_2_1_7_1","volume-title":"ACSL: ANSI\/ISO C Specification Language. CEA LIST and INRIA, 1.7 edition","author":"Baudin P.","year":"2013","unstructured":"P. Baudin , P. Cuoq , J.-C. Filli\u00e2tre , C. March\u00e9 , B. Monate , Y. Moy , and V. Prevosto . ACSL: ANSI\/ISO C Specification Language. CEA LIST and INRIA, 1.7 edition , 2013 . P. Baudin, P. Cuoq, J.-C. Filli\u00e2tre, C. March\u00e9, B. Monate, Y. Moy, and V. Prevosto. ACSL: ANSI\/ISO C Specification Language. CEA LIST and INRIA, 1.7 edition, 2013."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.5555\/2969951.2969968"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_10_1","DOI":"10.1145\/2429069.2429078"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.1145\/2400676.2400679"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_12_1","DOI":"10.1007\/978-3-642-28756-5_18"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_13_1","DOI":"10.1007\/11523468_109"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_14_1","DOI":"10.1007\/978-3-540-30579-8_8"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_15_1","DOI":"10.1007\/11817963_34"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_16_1","DOI":"10.1145\/1133981.1134029"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_18_1","DOI":"10.5555\/2958031.2958105"},{"key":"e_1_3_2_1_19_1","first-page":"19","volume-title":"Algorithmic Algebra and Logic: Proceedings of the A3L 2005 Conference in Honor of the 60th Birthday of Volker Weispfenning","author":"Hearn A. C.","year":"2005","unstructured":"A. C. Hearn . REDUCE : the first forty years. In A. Dolzmann, A. Seidl, and T. Sturm, editors , Algorithmic Algebra and Logic: Proceedings of the A3L 2005 Conference in Honor of the 60th Birthday of Volker Weispfenning , pages 19 -- 24 , Passau, Germany , 2005 . A. C. Hearn. REDUCE: the first forty years. In A. Dolzmann, A. Seidl, and T. Sturm, editors, Algorithmic Algebra and Logic: Proceedings of the A3L 2005 Conference in Honor of the 60th Birthday of Volker Weispfenning, pages 19--24, Passau, Germany, 2005."},{"key":"e_1_3_2_1_20_1","volume-title":"OFAI clp(Q,R)","author":"Holzbaur C.","year":"1995","unstructured":"C. Holzbaur . OFAI clp(Q,R) . Austrian Research Institute for Artificial Intelligence , Vienna , 1.3.3 edition, 1995 . Published as TR-95-09. C. Holzbaur. OFAI clp(Q,R). Austrian Research Institute for Artificial Intelligence, Vienna, 1.3.3 edition, 1995. Published as TR-95-09."},{"key":"e_1_3_2_1_21_1","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"259","volume-title":"Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA","author":"Otto C.","year":"2010","unstructured":"C. Otto , M. Brockschmidt , C. von Essen , and J. Giesl . Automated termination analysis of Java bytecode by term rewriting . In C. Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010 ), volume 6 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 259 -- 276 , Edinburgh, Scotland, UK , 2010. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik . C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl. Automated termination analysis of Java bytecode by term rewriting. In C. Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 259--276, Edinburgh, Scotland, UK, 2010. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik."},{"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\n   and Abstract Interpretation: Proceedings of the 5th International Conference (VMCAI \n  2004\n  ) volume \n  2937\n   of \n  Lecture Notes in Computer Science pages \n  239\n  --\n  251 Venice Italy 2004. \n  Springer\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: Proceedings of the 5th International Conference (VMCAI 2004) volume 2937 of Lecture Notes in Computer Science pages 239--251 Venice Italy 2004. Springer.","key":"e_1_3_2_1_22_1","DOI":"10.1007\/978-3-540-24622-0_20"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1145\/113413.113433"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_24_1","DOI":"10.1145\/1709093.1709095"},{"key":"e_1_3_2_1_25_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-540-27813-9_6","volume-title":"Computer Aided Verification: Proceedings of the 16th International Conference (CAV","author":"Tiwari A.","year":"2004","unstructured":"A. Tiwari . Termination of linear programs . In R. Alur and D. Peled, editors, Computer Aided Verification: Proceedings of the 16th International Conference (CAV 2004 ), volume 3114 of Lecture Notes in Computer Science , pages 70 -- 82 , Boston, MA , USA, 2004. Springer . A. Tiwari. Termination of linear programs. In R. Alur and D. Peled, editors, Computer Aided Verification: Proceedings of the 16th International Conference (CAV 2004), volume 3114 of Lecture Notes in Computer Science, pages 70--82, Boston, MA, USA, 2004. Springer."},{"key":"e_1_3_2_1_26_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/978-3-642-38856-9_5","volume-title":"Proceedings of the 20th International Symposium on Static Analysis (SAS","author":"Urban C.","year":"2013","unstructured":"C. Urban . The abstract domain of segmented ranking functions . In F. Logozzo and M. Fahndrich, editors, Proceedings of the 20th International Symposium on Static Analysis (SAS 2013 ), volume 7935 of Lecture Notes in Computer Science , pages 43 -- 62 , Seattle, WA , USA, 2013. Springer . C. Urban. The abstract domain of segmented ranking functions. In F. Logozzo and M. Fahndrich, editors, Proceedings of the 20th International Symposium on Static Analysis (SAS 2013), volume 7935 of Lecture Notes in Computer Science, pages 43--62, Seattle, WA, USA, 2013. Springer."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_27_1","DOI":"10.1007\/978-3-642-33125-1_28"}],"event":{"sponsor":["Universidad Complutense de Madrid","SIGPLAN ACM Special Interest Group on Programming Languages"],"acronym":"PPDP '13","name":"PPDP '13: 15th International Symposium on Principles and Practice of Declarative Programming","location":"Madrid Spain"},"container-title":["Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2505879.2505884","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2505879.2505884","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:34:16Z","timestamp":1750232056000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2505879.2505884"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,16]]},"references-count":25,"alternative-id":["10.1145\/2505879.2505884","10.1145\/2505879"],"URL":"https:\/\/doi.org\/10.1145\/2505879.2505884","relation":{},"subject":[],"published":{"date-parts":[[2013,9,16]]},"assertion":[{"value":"2013-09-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}