BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Translation Validation for LLVM's AArch64 Backend - John Regehr - 
 University of Utah
DTSTART:20250605T140000Z
DTEND:20250605T150000Z
UID:TALK231601@talks.cam.ac.uk
CONTACT:Luisa Cicolini
DESCRIPTION:Alive2 is a practical oracle for determining whether a transfo
 rmation on LLVM IR is a refinement -- that is\, whether it is valid under 
 the rules for LLVM optimizations. In this talk I'll describe an analogous 
 translation validation solution for LLVM's AArch64 backend that we've used
  to find 42 miscompilation bugs\, many of which were in architecture-neutr
 al code and hence could have also affected other backends. Our tool\, arm-
 tv\, reuses Alive2 as a source of LLVM semantics and offers a choice of tw
 o AArch64 semantics\, one that we wrote by hand and the other derived from
  ARM's machine readable specification of their ISA.\n\n*John Regehr* is a 
 computer science professor at the University of Utah\, USA. He liked to bu
 ild tools for compiler developers to use\, and then write papers about the
 m.\n\nIf you want to attend the compiler social\, please remember to sign 
 up: https://grosser.science/compiler-social-2025-06-05/
LOCATION:Computer Laboratory\, William Gates Building\, LT1
END:VEVENT
END:VCALENDAR