Formally verified big step semantics out of x86-64 binaries. - Ian Roessle; Freek Verbeek; Binoy Ravindran (CPP, 2019)

Establishing a refinement relation between binaries and abstract code. - Freek Verbeek; Joshua A. Bockenek; Abhijith Bharadwaj; Binoy Ravindran; Ian Roessle (MEMOCODE, 2019)

X86 instruction semantics and basic block symbolic execution. - Freek Verbeek; Abhijith Bharadwaj; Joshua A. Bockenek; Ian Roessle; Timmy Weerwag; Binoy Ravindran (Arch. Formal Proofs, 2021)

Toward Bridging the Semantic Gap Between x86-64 Software Binaries and Abstract Languages for Formal Verification and Security. - Ian Roessle (2025)