NEW: We are hiring Postdocs and PhD students!
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.
- A Widening Approach to Multi-Threaded Program Verification
- Lost in Abstraction: Monotonicity in Multi-Threaded Programs
- Don't sit on the fence: A static analysis approach to automatic fence insertion
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
- Ranking Function Synthesis for Bit-Vector Relations
- Symbolic Counter Abstraction for Concurrent Software
- Verification and Falsification of Programs with Loops using Predicate Abstraction
A previous version of this paper has appeared at CAV.
- A Survey of Automated Techniques for Formal Software Verification
- Deciding Bit-Vector Arithmetic with Abstraction
A previous version of this paper has appeared at TACAS.
- A Tool for Checking ANSI-C Programs
- Predicate Abstraction of ANSI-C Programs using SAT
- 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
- Object Oriented Design
- Software Verification
- Computer-Aided Formal Verification
- Computer Architecture