Research

I am interested in automated reasoning for verification of hardware and software. My main focus is on model checking safety properties of reactive systems, where I have employed a variety of methods, such as first-order reasoning, effectively propositional reasoning (EPR), satisfiability modulo theories (SMT) and propositional solving (SAT).

At MathWorks I am using this background to enhance the Simulink Design Verifier with new capabilities, and to make it scale to ever larger models our customers are coming up with.

Before, I have worked with Cesare Tinelli on model checking safety properties of software in the dataflow language Lustre using the Kind 2 model checker. By querying an SMT solver, the system can prove safety properties over typed streams. The system is a from scratch reimplementation of ideas from the PKIND system on a new extensible, parallel architecture. It enables the model checking eniges of k-induction, bounded model checking, and the newly added IC3 to cooperate during their proof procedures, while making use of template-based invariant discovery.

In my PhD project and after I have worked on automated reasoning with first-order instantiation-based methods and there in particular on handling theories like equality and beyond in a robust way. For this I have extended the iProver system as iProver-Eq integrating an SMT solver for ground reasoning and a labeled superposition-based calculus for first-order reasoning modulo equality.

We have also applied both the iProver and iProver-Eq systems for bounded model checking to verify safety properties of hardware designs with bitvectors and memories.

If this was too much jargon, please read the lay abstract of my PhD work, which is still not completely out of date.