Research
My research sits at the crossroads between theoretical computer science, software engineering, and artificial intelligence (AI) with a focus on formal methods for dependability analysis of complex cyber-physical systems. I am particularly interested in explainable formal methods and AI, probabilistic model checking, symbolic methods, and the formal analysis of configurable and reconfigurable software systems.
A recurring theme in my work is explainability: developing formal methods that are not only verifying system properties but are also comprehensible. This connects my work on formal verification, causality theory, and decision diagrams.
Projects
Current
- NWO VENI — Symbolic Verification and Explainability
- Center for Perspicuous Computing (CPEC) — Collaborative Research Center 248
Past
- Centre for Tactile Internet with Human-in-the-loop (CeTI) — Cluster of Excellence in the German Excellence Initiative
- Highly Adaptive Efficiency Computing (HAEC) — Collaborative Research Center 912
Tools
A framework for decision diagrams written in Rust. Supports safe, concurrent, modular, and performant decision diagram construction. EASST best paper award.
Main developer: Nils Husung
Computes causes for outcomes of Boolean functions, providing partial interpretations — so-called feature causes — from propositional logic formulas.
An explicit CTL model checker for recursive state machines using lazy evaluation to speed up analysis.
Main developer: Patrick Wienhöft
A language and tool for describing and analyzing (probabilistic) feature-oriented systems and software product lines. Generates compositional family models in Prism language.
Main developer: Philipp Chrszon
aMeSGee
A Java tool for quantitative message sequence graphs (qMSGs), enabling model checking of CSL properties for compositional qMSGs. Contact me if you are interested.