NEW: We are hiring PhD students!
NEW: Springer is now shipping the 2nd edition of the book on Decision Procedures!
I am interested in formal methods for the correct construction of hardware and software systems, with a focus on automated methods for checking compliance of an implementation with a specification. Techniques include model checking and automated testing.
I am particularly interested in applying these methods to practical hard- and software implementations given in languages like C/C++/Java, or HDLs such as Verilog and SystemC.
A full list of my papers is available here.
- Heap Layout Optimisation for Exploitation
- JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
- Model Checking Boot Code from AWS Data Centers
- Counterexample Guided Inductive Synthesis Modulo Theories
- Verification of Tree-Based Hierarchical Read-Copy Update in the Linux Kernel
- Efficient Verification of Multi-Property Designs (best paper in the design track)
- Program Synthesis for Program Analysis
- A Survey of Automated Techniques for Formal Software Verification
- A Tool for Checking ANSI-C Programs
Member of the steering committee of CAV.
Co-Chair of FLOC 2018.
I am Editor-in-Chief of Formal Methods in System Design.
- 15-820A: Theorem Proving and Model Checking in PVS (Spring 2003)
- 17-651A: Models of Software Systems (Fall 2003)
- 251-0247-00 Formal Verification
- 251-0207-00 Seminar Digitaltechnik und Rechnerarchitektur
- 251-0211-00 Spezifikation und Verifikation objektorientierter Software
- 252-0014-00 Digitaltechnik
- 251-0276-00 Software Engineering Seminar