~/talk

Translation Validation for LLVM's AArch64 Backend

on YouTube 15m
Talkat OOPSLA 2025 · 2025-10-16..10-18· [compilers-and-language-design]

speakers

name:Ryan Berger
links:none on file
name:Mitch Briles
github:MitchBriles
name:Nader Boushehrinejad Moradi
links:none on file
name:Nicholas Coughlin
links:none on file
name:Kait Lam
links:none on file
name:Nuno P. Lopes
links:none on file
name:Stefan Mada
links:none on file
name:Tanmay Tirpankar
links:none on file
name:John Regehr
website:http://www.cs.utah.edu/~regehr/

resources

video:https://youtu.be/EFywX-qFbyA
slides:none on file

summary

arm-tv is a translation validator that lifts AArch64 assembly to LLVM MIR, extends Alive2 to handle mixed pointer/integer code and adds a flat memory model and cross-model refinement checks, enforces numerous ABI rules, and uses partial evaluation over ARM’s machine‑readable spec to generate lifter code. The tool runs LLVM’s optimizer on the lifted IR and then checks refinement, finds and helps fix 45 bugs in the AArch64 backend, and flags ABI violations that caused real security issues.

AI-written summary · about

chapters (8)

  1. 0:00Compiler backend correctness
  2. 1:06LLVM AArch64 backend bug
  3. 3:16Translation validation
  4. 4:21ARM TV architecture
  5. 6:11Automating assembly lifter
  6. 8:00ABI compliance verification
  7. 9:27Memory model differences
  8. 11:11Conclusion

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.