{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T00:35:40Z","timestamp":1780706140271,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,4,17]],"date-time":"2021-04-17T00:00:00Z","timestamp":1618617600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1619275"],"award-info":[{"award-number":["1619275"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2996"],"award-info":[{"award-number":["N00014-17-1-2996"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,4,19]]},"DOI":"10.1145\/3445814.3446751","type":"proceedings-article","created":{"date-parts":[[2021,4,11]],"date-time":"2021-04-11T17:06:26Z","timestamp":1618160786000},"page":"1004-1019","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Language-parametric compiler validation with application to LLVM"],"prefix":"10.1145","author":[{"given":"Theodoros","family":"Kasampalis","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1551-2597","authenticated-orcid":false,"given":"Daejun","family":"Park","sequence":"additional","affiliation":[{"name":"Runtime Verification, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhengyao","family":"Lin","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0760-9690","authenticated-orcid":false,"given":"Vikram S.","family":"Adve","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,4,17]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2015. Instruction Selection load narrowing miscompilation. https:\/\/bugs.llvm. org\/show_bug.cgi?id= 4737.  2015. Instruction Selection load narrowing miscompilation. https:\/\/bugs.llvm. org\/show_bug.cgi?id= 4737."},{"key":"e_1_3_2_1_2_1","unstructured":"2015. Instruction Selection WAW miscompilation. https:\/\/bugs.llvm.org\/show_bug.cgi?id= 25154.  2015. Instruction Selection WAW miscompilation. https:\/\/bugs.llvm.org\/show_bug.cgi?id= 25154."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734"},{"key":"e_1_3_2_1_5_1","volume-title":"A LanguageIndependent Proof System for Mutual Program Equivalence","author":"Ciob\u00e2c\u0103 \u015etefan","unstructured":"\u015etefan Ciob\u00e2c\u0103 , Dorel Lucanu , Vlad Rusu , and Grigore Ro\u015fu . 2014. A LanguageIndependent Proof System for Mutual Program Equivalence . Springer International Publishing , Cham , 75-90. https:\/\/doi.org\/10.1007\/978-3-319-11737-9_6 10.1007\/978-3-319-11737-9_6 \u015etefan Ciob\u00e2c\u0103, Dorel Lucanu, Vlad Rusu, and Grigore Ro\u015fu. 2014. A LanguageIndependent Proof System for Mutual Program Equivalence. Springer International Publishing, Cham, 75-90. https:\/\/doi.org\/10.1007\/978-3-319-11737-9_6"},{"key":"e_1_3_2_1_6_1","volume-title":"Accessed","year":"2020","unstructured":"Clang. 2020 . Clang: C Language Family Frontend for LLVM. http:\/\/clang.llvm.org . Accessed : February 25, 2021. Clang. 2020. Clang: C Language Family Frontend for LLVM. http:\/\/clang.llvm.org. Accessed: February 25, 2021."},{"key":"e_1_3_2_1_7_1","volume-title":"iOS App Distribution Guide. https:\/\/developer.apple.com\/ library\/etc\/redirect\/DTS\/iOSAppDistGuide","author":"Apple Corp. 2019.","year":"2019","unstructured":"Apple Corp. 2019. iOS App Distribution Guide. https:\/\/developer.apple.com\/ library\/etc\/redirect\/DTS\/iOSAppDistGuide . Accessed : February 2019 . Apple Corp. 2019. iOS App Distribution Guide. https:\/\/developer.apple.com\/ library\/etc\/redirect\/DTS\/iOSAppDistGuide. Accessed: February 2019."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385964"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_10_1","volume-title":"GNU Compiler Collection Internals. https: \/\/gcc.gnu.org\/onlinedocs\/gccint\/Passes.html","author":"Foundation Free Software","year":"2020","unstructured":"Free Software Foundation . 2019. GNU Compiler Collection Internals. https: \/\/gcc.gnu.org\/onlinedocs\/gccint\/Passes.html . Accessed : August 2020 . Free Software Foundation. 2019. GNU Compiler Collection Internals. https: \/\/gcc.gnu.org\/onlinedocs\/gccint\/Passes.html. Accessed: August 2020."},{"key":"e_1_3_2_1_11_1","volume-title":"Accessed","author":"GCC.","year":"2020","unstructured":"GCC. 2020 . GNU Compiler Collection. https:\/\/gcc.gnu.org . Accessed : February 25, 2021. GCC. 2020. GNU Compiler Collection. https:\/\/gcc.gnu.org. Accessed: February 25, 2021."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3060140"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491442"},{"key":"e_1_3_2_1_14_1","unstructured":"Jeremy Horwitz. 2018. Apple Watch apps instantly went 64-bit thanks to obscure Bitcode option. VentureBeat ( 2018 ).  Jeremy Horwitz. 2018. Apple Watch apps instantly went 64-bit thanks to obscure Bitcode option. VentureBeat ( 2018 )."},{"key":"e_1_3_2_1_15_1","volume-title":"Intel 64 and IA-32 Architectures Software Developer's Manual","author":"Intel Corporation","unstructured":"Intel Corporation . 2016. Intel 64 and IA-32 Architectures Software Developer's Manual . Intel Corporation . Intel Corporation. 2016. Intel 64 and IA-32 Architectures Software Developer's Manual. Intel Corporation."},{"key":"e_1_3_2_1_16_1","volume-title":"Accessed","year":"2020","unstructured":"Julia. 2020 . The Julia Language. http:\/\/julialang.org . Accessed : February 25, 2021. Julia. 2020. The Julia Language. http:\/\/julialang.org. Accessed: February 25, 2021."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542513"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/977395.977673"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062343"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_22_1","volume-title":"Accessed","author":"LLVM.","year":"2020","unstructured":"LLVM. 2020 . LLVM Language Reference Manual. http:\/\/llvm.org\/docs\/LangRef. html . Accessed : February 25, 2021. LLVM. 2020. LLVM Language Reference Manual. http:\/\/llvm.org\/docs\/LangRef. html. Accessed: February 25, 2021."},{"key":"e_1_3_2_1_23_1","volume-title":"Accessed","author":"LLVM.","year":"2020","unstructured":"LLVM. 2020 . LLVM Target-Independent Code Generation: Instruction Selection. http:\/\/llvm.org\/docs\/CodeGenerator.html# instruction-selection-section . Accessed : February 25, 2021. LLVM. 2020. LLVM Target-Independent Code Generation: Instruction Selection. http:\/\/llvm.org\/docs\/CodeGenerator.html# instruction-selection-section. Accessed: February 25, 2021."},{"key":"e_1_3_2_1_24_1","volume-title":"Accessed","author":"LLVM.","year":"2020","unstructured":"LLVM. 2020 . LLVM Target-independent Code Generator. http:\/\/llvm.org\/docs\/ CodeGenerator.html# machine-code-representation . Accessed : February 25, 2021. LLVM. 2020. LLVM Target-independent Code Generator. http:\/\/llvm.org\/docs\/ CodeGenerator.html# machine-code-representation. Accessed: February 25, 2021."},{"key":"e_1_3_2_1_25_1","volume-title":"Accessed","author":"LLVM.","year":"2020","unstructured":"LLVM. 2020 . TableGen. http:\/\/llvm.org\/docs\/TableGen\/index.html . Accessed : February 25, 2021. LLVM. 2020. TableGen. http:\/\/llvm.org\/docs\/TableGen\/index.html. Accessed: February 25, 2021."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0058037"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_17"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_30_1","first-page":"151","volume-title":"Translation Validation. In Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS '98)","author":"Pnueli Amir","year":"1998","unstructured":"Amir Pnueli , Michael Siegel , and Eli Singerman . 1998 . Translation Validation. In Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS '98) . Springer-Verlag, London, UK, UK , 151 - 166 . http:\/\/dl.acm.org\/citation.cfm?id= 646482. 691453 Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation Validation. In Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS '98). Springer-Verlag, London, UK, UK, 151-166. http:\/\/dl.acm.org\/citation.cfm?id= 646482. 691453"},{"key":"e_1_3_2_1_31_1","volume-title":"Theory of Recursive Functions and Efective Computability","author":"Rogers Hartley","unstructured":"Hartley Rogers , Jr. 1987. Theory of Recursive Functions and Efective Computability . MIT Press , Cambridge, MA, USA . Hartley Rogers, Jr. 1987. Theory of Recursive Functions and Efective Computability. MIT Press, Cambridge, MA, USA."},{"key":"e_1_3_2_1_32_1","volume-title":"An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming 79, 6 ( 2010 ), 397-434. https:\/\/doi.org\/10.1016\/j.jlap","author":"Ro\u015fu Grigore","year":"2010","unstructured":"Grigore Ro\u015fu and Traian Florin \u015eerb\u0103nu\u0163\u0103 . 2010. An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming 79, 6 ( 2010 ), 397-434. https:\/\/doi.org\/10.1016\/j.jlap . 2010 . 03.012 10.1016\/j.jlap Grigore Ro\u015fu and Traian Florin \u015eerb\u0103nu\u0163\u0103. 2010. An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming 79, 6 ( 2010 ), 397-434. https:\/\/doi.org\/10.1016\/j.jlap. 2010. 03.012"},{"key":"e_1_3_2_1_34_1","volume-title":"Introduction to Bisimulation and Coinduction","author":"Sangiorgi Davide","unstructured":"Davide Sangiorgi . 2011. Introduction to Bisimulation and Coinduction . Cambridge University Press, New York, NY , USA. Davide Sangiorgi. 2011. Introduction to Bisimulation and Coinduction. Cambridge University Press, New York, NY, USA."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_2_1_36_1","first-page":"391","volume-title":"Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications (Indianapolis, Indiana, USA) ( OOPSLA '13). ACM","author":"Sharma Rahul","year":"2013","unstructured":"Rahul Sharma , Eric Schkufza , Berkeley Churchill , and Alex Aiken . 2013 . Datadriven Equivalence Checking . In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications (Indianapolis, Indiana, USA) ( OOPSLA '13). ACM , New York, NY, USA , 391 - 406 . https:\/\/doi.org\/10.1145\/2509136.2509509 10.1145\/2509136.2509509 Rahul Sharma, Eric Schkufza, Berkeley Churchill, and Alex Aiken. 2013. Datadriven Equivalence Checking. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications (Indianapolis, Indiana, USA) ( OOPSLA '13). ACM, New York, NY, USA, 391-406. https:\/\/doi.org\/10.1145\/2509136.2509509"},{"key":"e_1_3_2_1_37_1","volume-title":"SPEC CPU 2006 Benchmark. https:\/\/www.spec.org\/cpu2006\/. Accessed","author":"SPEC.","year":"2020","unstructured":"SPEC. 2020 . SPEC CPU 2006 Benchmark. https:\/\/www.spec.org\/cpu2006\/. Accessed : February 25, 2021. SPEC. 2020. SPEC CPU 2006 Benchmark. https:\/\/www.spec.org\/cpu2006\/. Accessed: February 25, 2021."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2931037"},{"key":"e_1_3_2_1_39_1","volume-title":"Accessed","year":"2020","unstructured":"Swift. 2020 . Swift programming language. https:\/\/swift.org . Accessed : February 25, 2021. Swift. 2020. Swift programming language. https:\/\/swift.org. Accessed: February 25, 2021."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993533"},{"key":"e_1_3_2_1_42_1","unstructured":"David Wheeler. 2015. To Bitcode or Not to Bitcode? iovation ( 2015 ).  David Wheeler. 2015. To Bitcode or Not to Bitcode? iovation ( 2015 )."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462164"},{"key":"e_1_3_2_1_44_1","volume-title":"VOC: A methodology for the translation validation of optimizing compilers. Journal of Universal Computer Science 9 ( 2003 )","author":"Zuck Lenore","year":"2003","unstructured":"Lenore Zuck , Amir Pnueli , Yi Fang , and Benjamin Goldberg . 2003 . VOC: A methodology for the translation validation of optimizing compilers. Journal of Universal Computer Science 9 ( 2003 ) , 2003. Lenore Zuck, Amir Pnueli, Yi Fang, and Benjamin Goldberg. 2003. VOC: A methodology for the translation validation of optimizing compilers. Journal of Universal Computer Science 9 ( 2003 ), 2003."}],"event":{"name":"ASPLOS '21: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","location":"Virtual USA","acronym":"ASPLOS '21","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3445814.3446751","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3445814.3446751","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3445814.3446751","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3445814.3446751","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:33Z","timestamp":1750195473000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3445814.3446751"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,17]]},"references-count":43,"alternative-id":["10.1145\/3445814.3446751","10.1145\/3445814"],"URL":"https:\/\/doi.org\/10.1145\/3445814.3446751","relation":{},"subject":[],"published":{"date-parts":[[2021,4,17]]},"assertion":[{"value":"2021-04-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}