We develop methods and tools to rigorously engineer zero-bug systems.

Formal Methods

We research mathematical methods and tools to ensure that systems have no functional or security bugs. This includes test case generation, model checking, automatic debugging, and automatic synthesis of systems from properties. Our interests include safe AI and security.
Team Bloem
We research formal methods for system design. We look at both functional properties and at security properties. For example, we develop methods to ensure that machine learning systems fulfill certain formal properties, or that systems are not vulnerable to power sidechannel or fault injection attacks. We use mathematical methods and create software tools to automatically prove correctness. One of our specialties is reactive synthesis: methods and tools that automatically generate correct systems from their specs. We publish at conferences like Computer Aided Verification (CAV) and Formal Methods for Computer Aided Design (FMCAD).

Team Members