{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:47:45Z","timestamp":1775868465019,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,6,11]],"date-time":"2018-06-11T00:00:00Z","timestamp":1528675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Samsung Research Funding Center of Samsung Electronics","award":["SRFC-IT1502-07"],"award-info":[{"award-number":["SRFC-IT1502-07"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,6,11]]},"DOI":"10.1145\/3192366.3192377","type":"proceedings-article","created":{"date-parts":[[2018,6,12]],"date-time":"2018-06-12T08:16:01Z","timestamp":1528791361000},"page":"631-645","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Crellvm: verified credible compilation for LLVM"],"prefix":"10.1145","author":[{"given":"Jeehoon","family":"Kang","sequence":"first","affiliation":[{"name":"Seoul National University, South Korea"}]},{"given":"Yoonseung","family":"Kim","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}]},{"given":"Youngju","family":"Song","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}]},{"given":"Juneyoung","family":"Lee","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}]},{"given":"Sanghoon","family":"Park","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}]},{"given":"Mark Dongyeon","family":"Shin","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}]},{"given":"Yonghyun","family":"Kim","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}]},{"given":"Sungkeun","family":"Cho","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}]},{"given":"Joonwon","family":"Choi","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}]},{"given":"Kwangkeun","family":"Yi","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}]}],"member":"320","published-online":{"date-parts":[[2018,6,11]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"Supplementary material for this paper available at http:\/\/sf.snu.ac.kr\/ crellvm\/ . Supplementary material for this paper available at http:\/\/sf.snu.ac.kr\/ crellvm\/ ."},{"key":"e_1_3_2_2_2_1","unstructured":"Andrew W. Appel. 2001. Foundational Proof-Carrying Code (LICS \u201901). Andrew W. Appel. 2001. Foundational Proof-Carrying Code (LICS \u201901)."},{"key":"e_1_3_2_2_3_1","unstructured":"The Coq Proof Assistant. https:\/\/coq.inria.fr\/ . The Coq Proof Assistant. https:\/\/coq.inria.fr\/ ."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2579080"},{"key":"e_1_3_2_2_5_1","volume-title":"SPEC CINT2006 Benchmark. https:\/\/www.spec.org\/cpu2006\/ CINT2006\/ .","author":"The","unstructured":"The SPEC CINT2006 Benchmark. https:\/\/www.spec.org\/cpu2006\/ CINT2006\/ . The SPEC CINT2006 Benchmark. https:\/\/www.spec.org\/cpu2006\/ CINT2006\/ ."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462173"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Delphine Demange David Pichardie and L\u00e9o Stefanesco. 2016. Verifying Fast and Sparse SSA-Based Optimizations in Coq (CC \u201916). Delphine Demange David Pichardie and L\u00e9o Stefanesco. 2016. Verifying Fast and Sparse SSA-Based Optimizations in Coq (CC \u201916).","DOI":"10.1007\/978-3-662-46663-6_12"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491442"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103666"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738005"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062343"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_18_1","unstructured":"Xavier Leroy Andrew W. Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert Memory Model Version 2. Research report RR-7987. INRIA. Xavier Leroy Andrew W. Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert Memory Model Version 2. Research report RR-7987. INRIA."},{"key":"e_1_3_2_2_19_1","unstructured":"LLVM Linux. http:\/\/llvm.linuxfoundation.org . LLVM Linux. http:\/\/llvm.linuxfoundation.org ."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062372"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"crossref","unstructured":"David Menendez Santosh Nagarakatte and Aarti Gupta. 2016. AliveFP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM (SAS \u201916). David Menendez Santosh Nagarakatte and Aarti Gupta. 2016. AliveFP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM (SAS \u201916).","DOI":"10.1007\/978-3-662-53413-7_16"},{"key":"e_1_3_2_2_23_1","volume-title":"Zuck","author":"Namjoshi Kedar S.","year":"2013","unstructured":"Kedar S. Namjoshi , Giacomo Tagliabue , and Lenore D . Zuck . 2013 . A Witnessing Compiler: A Proof of Concept (RV \u201913). Kedar S. Namjoshi, Giacomo Tagliabue, and Lenore D. Zuck. 2013. A Witnessing Compiler: A Proof of Concept (RV \u201913)."},{"key":"e_1_3_2_2_24_1","volume-title":"Zuck","author":"Namjoshi Kedar S.","year":"2013","unstructured":"Kedar S. Namjoshi and Lenore D . Zuck . 2013 . Witnessing Program Transformations (SAS \u201913). Kedar S. Namjoshi and Lenore D. Zuck. 2013. Witnessing Program Transformations (SAS \u201913)."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2590811"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"crossref","unstructured":"Amir Pnueli Michael Siegel and Eli Singerman. 1998. Translation Validation (TACAS \u201998). Amir Pnueli Michael Siegel and Eli Singerman. 1998. Translation Validation (TACAS \u201998).","DOI":"10.1007\/BFb0054170"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"crossref","unstructured":"Amir Pnueli Ofer Strichman and Michael Siegel. 1998. The Code Validation Tool CVT: Automatic Verification of a Compilation Process (STTT \u201998). Amir Pnueli Ofer Strichman and Michael Siegel. 1998. The Code Validation Tool CVT: Automatic Verification of a Compilation Process (STTT \u201998).","DOI":"10.1007\/s100090050027"},{"key":"e_1_3_2_2_30_1","unstructured":"HOL Interactive Theorem Prover. https:\/\/hol- theorem- prover.org\/ . HOL Interactive Theorem Prover. https:\/\/hol- theorem- prover.org\/ ."},{"key":"e_1_3_2_2_31_1","unstructured":"The Z3 Theorem Prover. https:\/\/github.com\/Z3Prover\/z3 . The Z3 Theorem Prover. https:\/\/github.com\/Z3Prover\/z3 ."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254104"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11970-5_13"},{"key":"e_1_3_2_2_34_1","volume-title":"Rinard and Darko Marinov","author":"Martin","year":"1999","unstructured":"Martin C. Rinard and Darko Marinov . 1999 . Credible Compilation with Pointers (RRV \u201999). Martin C. Rinard and Darko Marinov. 1999. Credible Compilation with Pointers (RRV \u201999)."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"crossref","unstructured":"Hanan Samet. 1978. Proving the Correctness of Heuristically Optimized Code (ACM \u201978). Hanan Samet. 1978. Proving the Correctness of Heuristically Optimized Code (ACM \u201978).","DOI":"10.1145\/359545.359569"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"crossref","unstructured":"Michael Stepp Ross Tate and Sorin Lerner. 2011. Equality-based Translation Validator for LLVM (CAV \u201911). Michael Stepp Ross Tate and Sorin Lerner. 2011. Equality-based Translation Validator for LLVM (CAV \u201911).","DOI":"10.1007\/978-3-642-22110-1_59"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806611"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993533"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328444"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542512"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706311"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462164"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"crossref","unstructured":"Lenore Zuck Amir Pnueli Benjamin Goldberg Clark Barrett Yi Fang and Ying Hu. 2002. Translation and Run-Time Validation of Loop Transformations (RV \u201902). Lenore Zuck Amir Pnueli Benjamin Goldberg Clark Barrett Yi Fang and Ying Hu. 2002. Translation and Run-Time Validation of Loop Transformations (RV \u201902).","DOI":"10.1016\/S1571-0661(04)80584-X"},{"key":"e_1_3_2_2_48_1","volume-title":"VOC: A Methodology for the Translation Validation of Optimizing Compilers (J. UCS \u201903).","author":"Zuck Lenore D.","year":"2003","unstructured":"Lenore D. Zuck , Amir Pnueli , and Benjamin Goldberg . 2003 . VOC: A Methodology for the Translation Validation of Optimizing Compilers (J. UCS \u201903). Lenore D. Zuck, Amir Pnueli, and Benjamin Goldberg. 2003. VOC: A Methodology for the Translation Validation of Optimizing Compilers (J. UCS \u201903)."}],"event":{"name":"PLDI '18: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Philadelphia PA USA","acronym":"PLDI '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192377","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192377","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T22:55:29Z","timestamp":1751669729000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192377"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,11]]},"references-count":48,"alternative-id":["10.1145\/3192366.3192377","10.1145\/3192366"],"URL":"https:\/\/doi.org\/10.1145\/3192366.3192377","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3296979.3192377","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2018,6,11]]},"assertion":[{"value":"2018-06-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}