Formal Methods Division

Our group performs research on the development and use of formal specification languages and verification approaches for different applications, including low- and high-level software, and (legal) contract analysis. Specification languages include classical and modal logics, and our verification techniques comprise model checking, automated reasoning, interactive theorem proving, static and runtime verification, and testing.

Our research projects

Our research areas

Verified Compilation

  • Verified Compilers: CakeML
  • Verified Machine Code

Formal Contracts

  • Contract Verification
  • Formalized Privacy Policies
  • Smart Contracts

Deductive Verification

  • Automatic Program Verifier
  • KeY: Java Verification
  • Intermediate Verification Language

Runtime Verification

  • Hybrid (static and runtime) Verification
  • Runtime Data and Control Properties

Theory Exploration

  • Hipster: Theory Exploration in Isabelle/HOL
  • Inductive Properties
  • TIP-Tools

Theorem Proving

  • Superposition Theorem Prover
  • Automatic Invariant Generation

Research Projects


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, 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

PolUser: Rich User-Controlled Privacy Policies

PolUser gives the data back to their real owners, not in the form of an asset that they can sell individually but rather to let them be in control of how much they want to share, how, when and under which circumstances their data may be used, and for which specific purpose.

To project website