Publications
- BIRD: A Binary Intermediate Representation for Formally Verified Decompilation of x86-64 Binaries. Daniel Engel, Freek Verbeek, and B. 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, Conditionally accepted.
- 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), Conditionally accepted, 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.