Research Projects / Tools


CakeML is a functional programming language and an ecosystem of proofs and tools built around the language. The ecosystem includes a proven-correct compiler that can bootstrap itself.
To Project Website


Hipster is a system integrating theory exploration with the proof assistant Isabelle/HOL. Theory exploration is a technique for automatically discovering new interesting lemmas in a given theory development.
To Project Website


Automatic theorem proving has a number of important applications, such as software verification, hardware verification, hardware design, knowledge representation and reasoning, the Semantic Web, algebra, and proving theorems in mathematics.
Vampire is an automatic theorem prover, that is, a system able to prove theorems. More precisely, it proves theorems in first-order logic.
To Project Website

KeY Project

KeY is an Java verification tool which let you specify the desired behavior of your program in the well-known specification language JML, and helps you proving that your programs conforms to its specification.
To Project Website


Initiation Grant on Runtime Verification for Autonomous Systems
April 2019 - March 2020
To Project Website


Period: Jan 2016 - Dec 2020
To Project Website


Period: Jan 2013 - Dec 2017
To Project Website


Period: Period: Jan 2012 - Dec 2017
To Project Website


Period: Jan 2013 - Dec 2016
To Project Website