Research Projects / Tools

CakeML

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

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

Vampire

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

STINT

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

PolUser

Period: Jan 2016 - Dec 2020
To Project Website

ReMU

Period: Jan 2013 - Dec 2017
To Project Website

DataBIn

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

StaRVOOrS

Period: Jan 2013 - Dec 2016
To Project Website