{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:31:52Z","timestamp":1784845912353,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,1,7]],"date-time":"2008-01-07T00:00:00Z","timestamp":1199664000000},"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":[[2008,1,7]]},"DOI":"10.1145\/1328438.1328459","type":"proceedings-article","created":{"date-parts":[[2008,1,7]],"date-time":"2008-01-07T09:45:40Z","timestamp":1199699140000},"page":"147-158","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":83,"title":["Proving non-termination"],"prefix":"10.1145","author":[{"given":"Ashutosh","family":"Gupta","sequence":"first","affiliation":[{"name":"Max Planck Institute, Saarbruecken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"UC Los Angeles, Los Angeles, CA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[{"name":"Max Planck Institute, Saarbruecken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ru-Gang","family":"Xu","sequence":"additional","affiliation":[{"name":"UC Los Angeles, Los Angeles, CA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2008,1,7]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"Aho A.V.","year":"1986","unstructured":"A.V. Aho , R. Sethi , and J.D. Ullman . Compilers: Principles, Techniques, and Tools . Addison-Wesley , 1986 . A.V. Aho, R. Sethi, and J.D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_3_2_1_3_1","volume-title":"June","author":"Bloch Joshua","year":"2006","unstructured":"Joshua Bloch . Nearly all binary searches and mergesorts are broken , June 2006 . http:\/\/googleresearch.blogspot.com\/2006\/06\/extra-extra-read-all-about-it-nearly.html. Joshua Bloch. Nearly all binary searches and mergesorts are broken, June 2006. http:\/\/googleresearch.blogspot.com\/2006\/06\/extra-extra-read-all-about-it-nearly.html."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_109"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_3_2_1_6_1","first-page":"442","volume-title":"Proc. CAV, LNCS 2404","author":"Colon M.","year":"2002","unstructured":"M. Colon and H. Sipma . Practical methods for proving program termination . In Proc. CAV, LNCS 2404 , pages 442 -- 454 . Springer , 2002 . M. Colon and H. Sipma. Practical methods for proving program termination. In Proc. CAV, LNCS 2404, pages 442--454. Springer, 2002."},{"key":"e_1_3_2_1_7_1","first-page":"420","volume-title":"Proc. CAV, LNCS~2725","author":"Colon M.","year":"2003","unstructured":"M. Colon , S. Sankaranarayanan , and H.B. Sipma . Linear invariant generation using non-linear constraint solving . In Proc. CAV, LNCS~2725 , pages 420 -- 432 . Springer , 2003 . M. Colon, S. Sankaranarayanan, and H.B. Sipma. Linear invariant generation using non-linear constraint solving. In Proc. CAV, LNCS~2725, pages 420--432. Springer, 2003."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_30"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_36"},{"key":"e_1_3_2_1_12_1","first-page":"519","volume-title":"Proc. CAV, LNCS 4590","author":"Ganesh V.","year":"2007","unstructured":"V. Ganesh and D.L. Dill . A decision procedure for bit-vectors and arrays . In Proc. CAV, LNCS 4590 , pages 519 -- 531 . Springer , 2007 . V. Ganesh and D.L. Dill. A decision procedure for bit-vectors and arrays. In Proc. CAV, LNCS 4590, pages 519--531. Springer, 2007."},{"key":"e_1_3_2_1_13_1","volume-title":"BUGS'2005 (PLDI'2005 Workshop on the Evaluation of Software Defect Detection Tools)","author":"Godefroid P.","year":"2005","unstructured":"P. Godefroid . The soundness of bugs is what matters (position statement) . In BUGS'2005 (PLDI'2005 Workshop on the Evaluation of Software Defect Detection Tools) , 2005 . P. Godefroid. The soundness of bugs is what matters (position statement). In BUGS'2005 (PLDI'2005 Workshop on the Evaluation of Software Defect Detection Tools), 2005."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181790"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_17_1","volume-title":"Edition 1.3.3","author":"Holzbaur C.","year":"1995","unstructured":"C. Holzbaur . OFAI clp(q,r) Manual , Edition 1.3.3 . Austrian Research Institute for Artificial Intelligence , Vienna , 1995 . TR-95-09. C. Holzbaur. OFAI clp(q,r) Manual, Edition 1.3.3. Austrian Research Institute for Artificial Intelligence, Vienna, 1995. TR-95-09."},{"key":"e_1_3_2_1_19_1","first-page":"295","volume":"2694","author":"Kremenek T.","year":"2003","unstructured":"T. Kremenek and D.R. Engler . Z-ranking: Using statistical analysis to counter the impact of static analysis approximations. In Proc. SAS, LNCS 2694 , pages 295 -- 315 . Springer, 2003 . T. Kremenek and D.R. Engler. Z-ranking: Using statistical analysis to counter the impact of static analysis approximations. In Proc. SAS, LNCS 2694, pages 295--315. Springer, 2003.","journal-title":"In Proc. SAS, LNCS"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.02.005"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964028"},{"key":"e_1_3_2_1_22_1","volume-title":"Theory of Linear and Integer Programming","author":"Schrijver A.","year":"1986","unstructured":"A. Schrijver . Theory of Linear and Integer Programming . Wiley , 1986 . A. Schrijver. Theory of Linear and Integer Programming. Wiley, 1986."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/998675.999446"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_2_1_25_1","volume-title":"Automatic non-termination analysis of imperative programs. Master's thesis","author":"Velroyen H.","year":"2007","unstructured":"H. Velroyen . Automatic non-termination analysis of imperative programs. Master's thesis , Chalmers University of Technology, Aachen Technical University , 2007 . H. Velroyen. Automatic non-termination analysis of imperative programs. Master's thesis, Chalmers University of Technology, Aachen Technical University, 2007."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/605397.605429"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095810.1095814"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_13"}],"event":{"name":"POPL08: The 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"San Francisco California USA","acronym":"POPL08","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1328438.1328459","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1328438.1328459","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:56:07Z","timestamp":1750240567000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1328438.1328459"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1,7]]},"references-count":27,"alternative-id":["10.1145\/1328438.1328459","10.1145\/1328438"],"URL":"https:\/\/doi.org\/10.1145\/1328438.1328459","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1328897.1328459","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2008,1,7]]},"assertion":[{"value":"2008-01-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}