# 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