Publications

On Extending Incorrectness Logic with Backwards Reasoning. Freek Verbeek, Md. Syadus Sefat, Zhoulai Fu, and Binoy Ravindran, 52nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2025), January 19-25, 2025, Denver, Colorado, USA.
Verifiably Correct Lifting of Position-Independent x86-64 Binaries to Symbolized Assembly. Freek Verbeek, Nico Naus, and Binoy Ravindran, 31st ACM Conference on Computer and Communications Security (CCS 2024), October 14-18, 2024, Salt Lake City, USA.
libLISA: Instruction Discovery and Analysis on x86-64. Jos Craaijo, Freek Verbeek, and Binoy Ravindran, 2024 ACM SIGPLAN Conference on Objected Oriented Programming, Systems, Languages and Applications (OOPSLA 2024), October 20-25, 2024, Pasadena, California, USA.
On the Decidability of Disassembling Binaries. Daniel Engel, Freek Verbeek, and Binoy Ravindran, 18th Theoretical Aspects of Software Engineering Conference (TASE 2024), July 29-August 1, 2024, Guiyang, China.
Exceptional Interprocedural Control Flow Graphs for x86-64 Binaries. Joshua Bockenek, Freek Verbeek, and Binoy Ravindran, 21st Conference on Detection of Intrusions and Malware & Vulnerability Assessment (DIMVA 2024), July 17-19, 2024, Lausanne, Switzerland.
BIRD: A Binary Intermediate Representation for Formally Verified Decompilation of x86-64 Binaries. Daniel Engel, Freek Verbeek, and Binoy Ravindran, 17th International Conference on Tests and Proofs (TAP 2023), July 18-19, 2023, Leicester, United Kingdom.
Low-level Reachability Analysis based on Formal Logic. Nico Naus, Freek Verbeek, Marc Schoolderman, and Binoy Ravindran, 17th International Conference on Tests and Proofs (TAP 2023), July 18-19, 2023, Leicester, United Kingdom.
A Formal Semantics for P-Code. Nico Naus, Freek Verbeek, and Binoy Ravindran, 14th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2022), October 17-18, 2022, Trento, Italy.
DSV: Disassembly Soundness Validation without Assuming a Ground Truth. Xiaoxin An, Freek Verbeek, and Binoy Ravindran, 14th NASA Formal Methods Symposium (NFM 2022), May 24-27, 2022, Pasadena, California, USA.
Formally Verified Lifting of C-compiled x86-64 Binaries. Freek Verbeek, Joshua A. Bockenek, Zhoulai Fu, and Binoy Ravindran, 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2022), June 13-17, 2022, San Diego, California, USA.
Verification of Functional Correctness of Code Diversification Techniques. Jae-Won Jang, Freek Verbeek, and Binoy Ravindran, 13th NASA Formal Methods Symposium (NFM 2021), May 24-28, 2021, Virtual.
x86 Instruction Semantics and Basic Block Symbolic Execution. Freek Verbeek, Abhijith Bharadwaj, Joshua A. Bockenek, Ian Roessle, Timmy Weerwag, and Binoy Ravindran, Archive of Formal Proofs, October 2021, Formal proof development, ISSN: 2150-914x.
Sound C Code Decompilation for a Subset of x86-64 Binaries. Freek Verbeek, Pierre Olivier, and Binoy Ravindran, 18th International Conference on Software Engineering and Formal Methods (SEFM 2020), September 14-18, 2020, Amsterdam, The Netherlands.
A Validation Methodology for OCaml-PVS Translation. Xiaoxin An, Amer Tahat, and Binoy Ravindran, 12th NASA Formal Methods Symposium (NFM 2020), May 11-15, 2020, NASA Ames Research Center, Moffett Field, CA, USA.
Highly Automated Formal Proofs over Memory Usage of Assembly Code. Freek Verbeek, Joshua A. Bockenek, and Binoy Ravindran, 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), April 25-30, 2020, Dublin, Ireland.
Scalable Translation Validation of Unverified Legacy OS Code. Amer Tahat, Sarang Joshi, Pronnoy Goswami, and Binoy Ravindran, International Conference on Formal Methods in Computer-Aided Design (FMCAD 2019), October 22-25, 2019, San Jose, California, USA.
Establishing a Refinement Relation between Binaries and Abstract Code, Freek Verbeek, Joshua A. Bockenek, Abhijith Bharadwaj, Ian Roessle, and Binoy Ravindran, ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2019), Work-in-Progress, October 9-11, 2019, San Diego, USA.
Symbolic Execution of x86 Assembly in Isabelle/HOL, Freek Verbeek, Abhijith Bharadwaj, Joshua A. Bockenek, Ian Roessle, and Binoy Ravindran, Workshop on Instruction Set Architecture Specification (SpISA 2019), September 13, 2019, Portland, Oregon, USA.
Formal Verification of Memory Preservation of x86-64 Binaries. Joshua A. Bockenek, Freek Verbeek, Peter Lammich, and Binoy Ravindran, 38th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2019), September 10-13, 2019, Turku, Finland.
Formally Verified Big Step Semantics out of x86-64 Binaries, Ian Roessle, Freek Verbeek, and Binoy Ravindran, the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP’19), January 14-15, 2019, Cascais/Lisbon, Portugal.

Theses

Low-Level Static Analysis for Memory Usage and Control Flow Recovery, Joshua Bockenek, PhD Dissertation, February 2023
On Reducing the Trusted Computing Base in Binary Verification, Xiaoxin An, PhD Dissertation, May 2022
Explicit-State Model Checking of Concurrent x86-64 Assembly, Abhijith Bharadwaj, MS Thesis, May 2020
USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow, Joshua Bockenek, MS Thesis, December 2017