My experience is in formal methods and automated reasoning, and in building systems for software and hardware verification, following and advancing the state of the art, in order to scale to industrial-size problems provided by customers from academia and industry.
Previously, I was a postdoctoral researcher in formal methods with a focus on model checking for verification of hardware and software and in first-order automated theorem proving.
I have also taught several university-level courses on logic, foundations and programming languages as the sole responsible lecturer.
Happy New Year! I'm starting it by relocating to the headquarter of MathWorks in Natick near Boston. Same job, same colleagues, same challenges, just a better time zone.
I'm attending the CAV conference and workshops this year. I'll be in Toronto July 16-July 23 if you want to meet up.
I discovered a really nice event organized by MathWorks: the annual research faculty summit. Plenty of interesting research being presented, and encouragingly many people mentioned how important verification is for them.
Our tool paper about the Kind 2 model checker has been accepted at CAV. We discuss an improved invariant generation and introduce two new features: contract-based compositional reasoning and certificate generation. These features have been developed mainly by my co-authors who are still on the project, evolving my work on re-implementing Kind 2.
We are looking for another developer to join the Simulink Design Verifier team, see the job posting. Help us add new capabilities to the model checker for Simulink, which is used by big customers in many industries worldwide.
I took up the exciting opportunity to continue working on model checking in a bigger industrial context by joining MathWorks as a developer on the Simulink Design Verifier team. I will be working out of Munich, Germany, and I'm looking forward to it.
(E-mail me for a full CV)
Before joining The MathWorks, I was a Postdoctoral Research Scholar at the Department of Computer Science at the University of Iowa. With Cesare Tinelli we were working on techniques for model checking safety properties of software in the dataflow language Lustre using the Kind 2 model checker, funded by an AFRL and a NASA grant.
I was awarded a postdoctoral fellowship in the EPSRC PhD Plus scheme (now the EPSRC doctoral prize) at The University of Manchester, UK mentored by Konstantin Korovin. The goal was to investigate applications of my PhD research, and we worked on model checking for hardware verification with effectively propositional reasoning.
I obtained my PhD in Computer Science from The University of Manchester, UK under supervision of Konstantin Korovin and Renate Schmidt. My thesis is entitled “Efficient Equational Reasoning in the Inst-Gen Framework”. (PDF)
I graduated in Informatik (Computer Science) from the University of Karlsruhe (now the Karlsruhe Insititue of Technology, KIT) with a German “Diplom”, which used to be a 4.5 year course roughly equivalent to a combined BSc and MSc degree, and has now been replaced by those two degrees.
I wrote my final dissertation “Automated Theorem Proving in Interactive Proof Construction” (PDF) at the Australian National University, Canberra and NICTA under supervision of Peter Baumgartner (NICTA) and P. H. Schmitt (Uni Karlsruhe).