{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:58:16Z","timestamp":1790927896414,"version":"4.1.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n                    LLVM\u2019s backends translate its intermediate representation (IR) to assembly or object code. Alongside register allocation and instruction selection, these backends contain many analogues of components traditionally associated with compiler middle ends: dataflow analyses, common subexpression elimination, loop invariant code motion, and a first-class IR\u2014MIR, the \u201cmachine IR.\u201d In effect, this kind of compiler backend is a highly optimizing compiler in its own right, with all of the correctness hazards entailed by a million lines of intricate C++. As a step towards gaining confidence in the correctness of work done by LLVM backends, we have created\n                    <jats:sc>arm-tv,<\/jats:sc>\n                    which formally verifies translations between LLVM IR and AArch64 (64-bit ARM) code. Ours is not the first translation validation work for LLVM, but we have advanced the state of the art along multiple fronts:\n                    <jats:sc>arm-tv<\/jats:sc>\n                    is a checking validator that enforces numerous ABI rules; we have extended Alive2 (which we reuse as a verification backend) to deal with unstructured mixes of pointers and integers that are typical of assembly code; we investigate the tradeoffs between hand-written AArch64 semantics and those derived mechanically from ARM\u2019s published formal semantics; and, we have used\n                    <jats:sc>arm-tv<\/jats:sc>\n                    to discover 45 previously unknown miscompilation bugs in this LLVM backend, most of which are now fixed in upstream LLVM.\n                  <\/jats:p>","DOI":"10.1145\/3763147","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"2710-2735","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Translation Validation for LLVM\u2019s AArch64 Backend"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-0355-2009","authenticated-orcid":false,"given":"Ryan","family":"Berger","sequence":"first","affiliation":[{"name":"NVIDIA, Santa Clara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-8252-8814","authenticated-orcid":false,"given":"Mitch","family":"Briles","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-5095-368X","authenticated-orcid":false,"given":"Nader","family":"Boushehrinejad Moradi","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8758-0666","authenticated-orcid":false,"given":"Nicholas","family":"Coughlin","sequence":"additional","affiliation":[{"name":"Defence Science and Technology Group, Brisbane, Australia"},{"name":"University of Queensland, Brisbane, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-2599-2259","authenticated-orcid":false,"given":"Kait","family":"Lam","sequence":"additional","affiliation":[{"name":"Defence Science and Technology Group, Brisbane, Australia"},{"name":"University of Queensland, Brisbane, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3160-1672","authenticated-orcid":false,"given":"Nuno P.","family":"Lopes","sequence":"additional","affiliation":[{"name":"INESC-ID, Lisbon, Portugal"},{"name":"Instituto Superior T\u00e9cnico - University of Lisbon, Lisbon, Portugal"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-8473-3667","authenticated-orcid":false,"given":"Stefan","family":"Mada","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0049-5045","authenticated-orcid":false,"given":"Tanmay","family":"Tirpankar","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7025-4610","authenticated-orcid":false,"given":"John","family":"Regehr","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Sandeep Dasgupta Sushant Dinesh Deepan Venkatesh Vikram S. Adve and Christopher W. Fletcher. 2020. Scalable validation of binary lifters. In PLDI. doi:10.1145\/3385412.3385964","DOI":"10.1145\/3385412.3385964"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Yuyou Fan and John Regehr. 2024. High-Throughput Formal-Methods-Assisted Fuzzing for LLVM. In CGO. doi:10.1109\/CG057630.2024.10444854","DOI":"10.1109\/CG057630.2024.10444854"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729275"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Seungwan Kwon Jaeseong Kwon Wooseok Kang Juneyoung Lee and Kihong Heo. 2024. Translation Validation for JIT Compiler in the V8 JavaScript Engine. In ICSE. doi:10.1145\/3597503.3639189","DOI":"10.1145\/3597503.3639189"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Kait Lam and Nicholas Coughlin. 2023. Lift-off: Trustworthy ARMv8 semantics from formal specifications. In FMCAD. doi:10.34727\/2023\/isbn.978-3-85448-060-0_36","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_36"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Vu Le Mehrdad Afshari and Zhendong Su. 2014. Compiler validation via equivalence modulo inputs. In PLDI. doi:10.1145\/2594291.2594334","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276495"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Juneyoung Lee Dongjoo Kim Chung-Kil Hur and Nuno P. Lopes. 2021. An SMT Encoding of LLVM\u2019s Memory Model for Bounded Translation Validation. In CAV. doi:10.1007\/978-3-030-81688-9_35","DOI":"10.1007\/978-3-030-81688-9_35"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"Juneyoung Lee Yoonseung Kim Youngju Song Chung-Kil Hur Sanjoy Das David Majnemer John Regehr and Nuno P. Lopes. 2017. Taming Undefined Behavior in LLVM. In PLDI. doi:10.1145\/3062341.3062343","DOI":"10.1145\/3062341.3062343"},{"key":"e_1_3_2_11_2","unstructured":"Arm Limited. 2025. Arm A64 Instruction Set for A-profile architecture. https:\/\/www.arm.com\/architecture\/cpu\/a-profile"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","unstructured":"Zhibo Liu Yuanyuan Yuan Shuai Wang and Yuyan Bao. 2022. SoK: Demystifying Binary Lifters Through the Lens of Downstream Applications. In IEEE SP. doi:10.1109\/SP46214.2022.9833799","DOI":"10.1109\/SP46214.2022.9833799"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428264"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Nuno P. Lopes Juneyoung Lee Chung-Kil Hur Zhengyang Liu and John Regehr. 2021. Alive2: bounded translation validation for LLVM. In PLDI. doi:10.1145\/3453483.3454030","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"George C. Necula. 2000. Translation validation for an optimizing compiler. In PLDI. doi:10.1145\/349299.349314","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Amir Pnueli Michael Siegel and Eli Singerman. 1998. Translation Validation. In TACAS. doi:10.1007\/BFb0054170","DOI":"10.1007\/BFb0054170"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Fr\u00e9d\u00e9ric Recoules S\u00e9bastien Bardin Richard Bonichon Laurent Mounier and Marie-Laure Potet. 2020. Get rid of inline assembly through verification-oriented lifting. In ASE. doi:10.1109\/ASE.2019.00060","DOI":"10.1109\/ASE.2019.00060"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Alastair Reid. 2016. Trustworthy specifications of ARM\u00ae v8-A and v8-M system level architecture. In FMCAD. doi:10.1109\/FMCAD.2016.7886675","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"e_1_3_2_19_2","doi-asserted-by":"crossref","unstructured":"Yuyang Rong Zhanghan Yu Zhenkai Weng Stephen Neuendorffer and Hao Chen. 2024. IRFuzzer: Specialized Fuzzing for LLVM Backend Code Generation. arXiv:2402.05256","DOI":"10.1109\/ICSE55347.2025.00130"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649863"},{"key":"e_1_3_2_21_2","unstructured":"Fabian Ruffy Tao Wang and Anirudh Sivaraman. 2020. Gauntlet: finding bugs in compilers for programmable packet processing. In OSDI. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/ruffy"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.5555\/907044"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Thomas Sewell Magnus Myreen and Gerwin Klein. 2013. Translation Validation for a Verified OS Kernel. In PLDI. doi:10.1145\/2491956.2462183","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Jean-Baptiste Tristan Paul Govereau and Greg Morrisett. 2011. Evaluating value-graph translation validation for LLVM. In PLDI. doi:10.1145\/1993498.1993533","DOI":"10.1145\/1993498.1993533"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Freek Verbeek Joshua Bockenek Zhoulai Fu and Binoy Ravindran. 2022. Formally verified lifting of C-compiled X86-64 binaries. In PLDI. doi:10.1145\/3519939.3523702","DOI":"10.1145\/3519939.3523702"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689755"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Xuejun Yang Yang Chen Eric Eide and John Regehr. 2011. Finding and understanding bugs in C compilers. In PLDI.doi:10.1145\/1993498.1993532","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Jianzhou Zhao Santosh Nagarakatte Milo M.K. Martin and Steve Zdancewic. 2013. Formal verification of SSA-based optimizations for LLVM. In PLDI. doi:10.1145\/2491956.2462164","DOI":"10.1145\/2491956.2462164"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763147","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:14:25Z","timestamp":1784196865000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763147"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":27,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763147"],"URL":"https:\/\/doi.org\/10.1145\/3763147","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-24","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}