Islaris: verification of machine code against authoritative ISA semantics

Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell 0001, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg 0001, Peter Sewell. Islaris: verification of machine code against authoritative ISA semantics. In Ranjit Jhala, Isil Dillig, editors, PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022. pages 825-840, ACM, 2022. [doi]

Abstract

Abstract is missing.