{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:05Z","timestamp":1772163965911,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,6,15]],"date-time":"2009-06-15T00:00:00Z","timestamp":1245024000000},"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":[[2009,6,15]]},"DOI":"10.1145\/1542476.1542512","type":"proceedings-article","created":{"date-parts":[[2009,6,16]],"date-time":"2009-06-16T09:34:36Z","timestamp":1245144876000},"page":"316-326","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":44,"title":["Verified validation of lazy code motion"],"prefix":"10.1145","author":[{"given":"Jean-Baptiste","family":"Tristan","sequence":"first","affiliation":[{"name":"INRIA Paris-Rocquencourt, Rocquencourt, France"}]},{"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[{"name":"INRIA Paris-Rocquencourt, Rocquencourt, France"}]}],"member":"320","published-online":{"date-parts":[[2009,6,15]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_29"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"phInteractive Theorem Proving and Program Development --- Coq'Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science","author":"Bertot Yves","year":"2004","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . phInteractive Theorem Proving and Program Development --- Coq'Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science . Springer , 2004 . Yves Bertot and Pierre Cast\u00e9ran. phInteractive Theorem Proving and Program Development --- Coq'Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, 2004."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277653"},{"key":"e_1_3_2_1_4_1","volume-title":"The Coq proof assistant. Software and documentation","author":"CoqCoq","year":"1989","unstructured":"CoqCoq development team. The Coq proof assistant. Software and documentation available at http:\/\/coq.inria.fr\/, 1989 --2009. CoqCoq development team. The Coq proof assistant. Software and documentation available at http:\/\/coq.inria.fr\/, 1989--2009."},{"key":"e_1_3_2_1_5_1","volume-title":"11th Int. Symp., SAS 2004","volume":"3148","author":"Gulwani Sumit","year":"2004","unstructured":"Sumit Gulwani and George C. Necula . A polynomial-time algorithm for global value numbering. In phStatic Analysis , 11th Int. Symp., SAS 2004 , volume 3148 of Lecture Notes in Computer Science, pages 212--227. Springer , 2004 . Sumit Gulwani and George C. Necula. A polynomial-time algorithm for global value numbering. In phStatic Analysis, 11th Int. Symp., SAS 2004, volume 3148 of Lecture Notes in Computer Science, pages 212--227. Springer, 2004."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_19"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2006.4"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/143095.143136"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/183432.183443"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2005.51"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781156"},{"key":"e_1_3_2_1_13_1","volume-title":"July","author":"Leroy Xavier","year":"2008","unstructured":"Xavier Leroy . A formally verified compiler back-end. arXiv:0902.2137 {cs} . Submitted, July 2008 . Xavier Leroy. A formally verified compiler back-end. arXiv:0902.2137 {cs}. Submitted, July 2008."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_3_2_1_16_1","volume-title":"The CompCert verified compiler. Development","author":"Xavier Leroy","year":"2004","unstructured":"Xavier Leroy et al. The CompCert verified compiler. Development available at http:\/\/compcert.inria.fr, 2004 --2009. Xavier Leroy et al. The CompCert verified compiler. Development available at http:\/\/compcert.inria.fr, 2004--2009."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/359060.359069"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_19_1","volume-title":"The code validation tool (CVT) -- automatic verification of a compilation process. phInternational Journal on Software Tools for Technology Transfer, 2: 192--201","author":"Pnueli Amir","year":"1998","unstructured":"Amir Pnueli , Ofer Shtrichman , and Michael Siegel . The code validation tool (CVT) -- automatic verification of a compilation process. phInternational Journal on Software Tools for Technology Transfer, 2: 192--201 , 1998 a. Amir Pnueli, Ofer Shtrichman, and Michael Siegel. The code validation tool (CVT) -- automatic verification of a compilation process. phInternational Journal on Software Tools for Technology Transfer, 2: 192--201, 1998a."},{"key":"e_1_3_2_1_20_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"TACAS'98","author":"Pnueli Amir","year":"1998","unstructured":"Amir Pnueli , Michael Siegel , and Eli Singerman . Translation validation. In phTools and Algorithms for Construction and Analysis of Systems , TACAS'98 , volume 1384 of Lecture Notes in Computer Science , pages 151 -- 166 . Springer , 1998 Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In phTools and Algorithms for Construction and Analysis of Systems, TACAS'98, volume 1384 of Lecture Notes in Computer Science, pages 151--166. Springer, 1998"},{"key":"e_1_3_2_1_21_1","volume-title":"Credible compilation with pointers. In phWorkshop on Run-Time Result Verification","author":"Rinard Martin","year":"1999","unstructured":"Martin Rinard and Darko Marinov . Credible compilation with pointers. In phWorkshop on Run-Time Result Verification , 1999 . Martin Rinard and Darko Marinov. Credible compilation with pointers. In phWorkshop on Run-Time Result Verification, 1999."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964002"},{"key":"e_1_3_2_1_23_1","volume-title":"Third International Symposium, SAS'96","volume":"1145","author":"Steffen Bernhard","year":"1996","unstructured":"Bernhard Steffen . Property-oriented expansion. In Static Analysis , Third International Symposium, SAS'96 , volume 1145 of Lecture Notes in Computer ScienceLNCS, pages 22--41. Springer , 1996 . Bernhard Steffen. Property-oriented expansion. In Static Analysis, Third International Symposium, SAS'96, volume 1145 of Lecture Notes in Computer ScienceLNCS, pages 22--41. Springer, 1996."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328444"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"},{"key":"e_1_3_2_1_27_1","volume-title":"VOC: A methodology for translation validation of optimizing compilers. phJournal of Universal Computer Science, 9 (3): 223--247","author":"Zuck Lenore","year":"2003","unstructured":"Lenore Zuck , Amir Pnueli , Yi Fang , and Benjamin Goldberg . VOC: A methodology for translation validation of optimizing compilers. phJournal of Universal Computer Science, 9 (3): 223--247 , 2003 . Lenore Zuck, Amir Pnueli, Yi Fang, and Benjamin Goldberg. VOC: A methodology for translation validation of optimizing compilers. phJournal of Universal Computer Science, 9 (3): 223--247, 2003."}],"event":{"name":"PLDI '09: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Dublin Ireland","acronym":"PLDI '09","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1542476.1542512","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1542476.1542512","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:29:49Z","timestamp":1750238989000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1542476.1542512"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6,15]]},"references-count":26,"alternative-id":["10.1145\/1542476.1542512","10.1145\/1542476"],"URL":"https:\/\/doi.org\/10.1145\/1542476.1542512","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1543135.1542512","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2009,6,15]]},"assertion":[{"value":"2009-06-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}