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 or C++, or HDLs such as Verilog and SystemC.
A full list of my papers is available here.
- NEW Numeric Bounds Analysis with Conflict-Driven Learning
- NEW Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs
- NEW Linear Completeness Thresholds for Bounded Model Checking
- Loop Summarization and Termination Analysis
- Termination Analysis with Compositional Transition Invariants
- Dynamic Cutoff Detection in Parameterized Concurrent Programs
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
- Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors
- 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
This paper is at rank 7 on this list.
- 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