Research

We study, develop, and apply formal methods to software systems, with a strong emphasis on tools that automate formal verification. Our foundational research spans concurrency theory, model checking, probabilistic computation, program analysis, and formal semantics.

Research highlights

Storm

A symbolic and explicit-state probabilistic model checker with a modular architecture and a Python interface. Storm supports models including dynamic fault trees and stochastic Petri nets.

Caesar

A deductive verifier for randomised algorithms, implemented in Rust. Its quantitative intermediate verification language and SMT backends support prototyping and combining verification techniques.

Prophesy

A tool supporting scalable parameter synthesis for probabilistic models. Our techniques have automatically synthesised the optimal randomisation bias in Herman’s ring protocol, a self-stabilising distributed algorithm.

COMPASS

A comprehensive toolset for extended AADL, developed with FBK Trento and support from the European Space Agency. COMPASS applies probabilistic model checking in aerospace and has been validated on industrial case studies.

C-program verification and NITWIT

We have developed software model checking for C programs in automation and verified key automotive software components. NITWIT independently checks violation witnesses produced by software model checkers.

Attestor

Automated verification of Java programs operating on dynamic data structures. Attestor checks shape and correctness properties, supports procedure-modular reasoning, and gives visual feedback when properties are violated.

Reasoning about probabilistic programs

We develop weakest precondition calculi for expected runtime analysis and exact inference in probabilistic programs. Extensions of separation logic support proofs about randomised algorithms manipulating dynamic data structures.

Earlier projects

Publications

2026

2025

Browse all publications