{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:44:59Z","timestamp":1772163899293,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2006,6,11]],"date-time":"2006-06-11T00:00:00Z","timestamp":1149984000000},"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":[[2006,6,11]]},"DOI":"10.1145\/1133981.1134029","type":"proceedings-article","created":{"date-parts":[[2006,7,24]],"date-time":"2006-07-24T12:53:01Z","timestamp":1153745581000},"page":"415-426","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":221,"title":["Termination proofs for systems code"],"prefix":"10.1145","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[{"name":"Microsoft Research"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[{"name":"Max-Planck-Institut f\u00fcr Informatik"}]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[{"name":"Max-Planck-Institut f\u00fcr Informatik and EPFL"}]}],"member":"320","published-online":{"date-parts":[[2006,6,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_12"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217943"},{"key":"e_1_3_2_1_3_1","volume-title":"FMICS'02: Formal Methods for Industrial Critical Systems","author":"Biere A.","unstructured":"A. Biere , C. Artho , and V. Schuppan . Liveness checking as safety checking . In FMICS'02: Formal Methods for Industrial Critical Systems , volume 66(2) of ENTCS, 2002 . A. Biere, C. Artho, and V. Schuppan. Liveness checking as safety checking. In FMICS'02: Formal Methods for Industrial Critical Systems, volume 66(2) of ENTCS, 2002."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155095"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_8"},{"key":"e_1_3_2_1_8_1","series-title":"LNCS","first-page":"168","volume-title":"TACAS'04: Tools and Algorithms for the Construction and Analysis of Systems","author":"Clarke E.","year":"2004","unstructured":"E. Clarke , D. Kroening , and F. Lerda . A tool for checking ANSI-C programs . In TACAS'04: Tools and Algorithms for the Construction and Analysis of Systems , volume 2988 of LNCS , pages 168 -- 176 . Springer , 2004 . E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In TACAS'04: Tools and Algorithms for the Construction and Analysis of Systems, volume 2988 of LNCS, pages 168--176. Springer, 2004."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(99)00006-0"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734281"},{"key":"e_1_3_2_1_11_1","first-page":"71","volume-title":"Proving Termination of Rewriting with CiME. In Extended Abstracts of the 6th International Workshop on Termination, WST'03","author":"Contejean E.","year":"2003","unstructured":"E. Contejean , C. March\u00e9 , B. Monate , and X. Urbain . Proving Termination of Rewriting with CiME. In Extended Abstracts of the 6th International Workshop on Termination, WST'03 , pages 71 -- 73 , June 2003 . E. Contejean, C. March\u00e9, B. Monate, and X. Urbain. Proving Termination of Rewriting with CiME. In Extended Abstracts of the 6th International Workshop on Termination, WST'03, pages 71--73, June 2003."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_30"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_8"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"e_1_3_2_1_15_1","series-title":"Proceedings of Symposia in Applied Mathematics","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume-title":"Mathematical Aspects of Computer Science","author":"Floyd R. W.","year":"1967","unstructured":"R. W. Floyd . Assigning meanings to programs . In J. T. Schwartz, editor, Mathematical Aspects of Computer Science , volume 19 of Proceedings of Symposia in Applied Mathematics , pages 19 -- 32 . American Mathematical Society , 1967 . R. W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19--32. American Mathematical Society, 1967."},{"key":"e_1_3_2_1_16_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1007\/978-3-540-25979-4_15","volume-title":"RTA'2004: Rewriting Techniques and Applications","author":"Giesl J.","year":"2004","unstructured":"J. Giesl , R. Thiemann , P. Schneider-Kamp , and S. Falke . Automated termination proofs with AProVE . In RTA'2004: Rewriting Techniques and Applications , 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 RTA'2004: Rewriting Techniques and Applications, volume 3091 of LNCS, pages 210--220. Springer, 2004."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","first-page":"444","DOI":"10.1007\/3-540-63166-6_44","volume-title":"CAV'97: Computer-Aided Verification, LNCS","author":"Lindenstrauss N.","year":"1997","unstructured":"N. Lindenstrauss , Y. Sagiv , and A. Serebrenik . TermiLog: A system for checking termination of queries to logic programs . In CAV'97: Computer-Aided Verification, LNCS , pages 444 -- 447 . Springer , 1997 . N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. TermiLog: A system for checking termination of queries to logic programs. In CAV'97: Computer-Aided Verification, LNCS, pages 444--447. Springer, 1997."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/211468"},{"key":"e_1_3_2_1_21_1","volume-title":"July","author":"Microsoft Corporation","year":"2004","unstructured":"Microsoft Corporation . Windows Static Driver Verifier. Available at www.microsoft.com\/whdc\/devtools\/tools\/SDV.mspx , July 2004 . Microsoft Corporation. Windows Static Driver Verifier. Available at www.microsoft.com\/whdc\/devtools\/tools\/SDV.mspx, July 2004."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021840"},{"issue":"2","key":"e_1_3_2_1_24_1","first-page":"230","article-title":"On computable numbers, with an application to the Entscheidungsproblem","volume":"42","author":"Turing A.","year":"1936","unstructured":"A. Turing . On computable numbers, with an application to the Entscheidungsproblem . London Mathematical Society , 42 ( 2 ): 230 -- 265 , 1936 . A. Turing. On computable numbers, with an application to the Entscheidungsproblem. London Mathematical Society, 42(2):230--265, 1936.","journal-title":"London Mathematical Society"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765712.1765729"}],"event":{"name":"PLDI06: ACM SIGPLAN Conference on Programming Language Design and Implementation 2006","location":"Ottawa Ontario Canada","acronym":"PLDI06","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1133981.1134029","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1133981.1134029","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:06:30Z","timestamp":1750244790000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1133981.1134029"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,6,11]]},"references-count":25,"alternative-id":["10.1145\/1133981.1134029","10.1145\/1133981"],"URL":"https:\/\/doi.org\/10.1145\/1133981.1134029","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1133255.1134029","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2006,6,11]]},"assertion":[{"value":"2006-06-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}