NEW: We are hiring PhD students!
NEW: Springer is now shipping the 2nd edition of the book on Decision Procedures!
NEW: MIT Press is now shipping the 2nd edition of the Model Checking book!
I am interested in automated reasoning techniques for automating the development of software. I am particularly interested in applying these methods to practical hard- and software implementations given in languages like C/C++ or Java.
A full list of my papers is available here.
- Concolic Testing for Deep Neural Networks
- 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 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