This website is under construction
I am a researcher and have been a PostDoc at UC Berkeley since March 2020. I am part of the Learn and Verify Group, headed by Sanjit Seshia.
Previously, I was a PhD student at RWTH Aachen University, under the supervision of Joost-Pieter Katoen.
I defended my PhD thesis titled Parameter Synthesis in Markov Models (pdf) in February 2020.
I am broadly interested in the automatic analysis of critical systems. This interest includes modelling and verification aspects. In particular, I am interested in the analysis of models that explicitly model uncertainty.
Some models and methods I often work with are:
- (Probabilistic) Model checking and abstraction.
- SAT and SMT solvers.
- Markov decision processes (MDPs), in particular also parametric or partially observable MDPs.
- Fault trees, in particular their dynamic extensions.
For now, please refer to DBLP or Google Scholar for an overview of my publications.
Over the years, I’ve been involved in the development of the following tools to advance the state-of-the-art in computer aided verification:
- The probabilistic model checker Storm (since 2014) and its python bindings stormpy (since 2016)
- The parameter synthesis framework for Markov models PROPhESY (since 2014)
- The SMT-solver SMT-RAT (2011 — 2015)
- The arithmetic library carl (2012 — 2015) and its python bindings pycarl (since 2016)
- Compass (2014)
- RWTH ICT Young Researcher Award 2017
- Fakultätentag Informatik Preis 2015, awarded for the best CS-related Master Thesis at a German University.
I have given invited talks at:
Moreover, I have given (external) seminar talks at ISCAS (Beijing), IST Austria, LaBRI (Bordeaux), Stanford, UC Berkeley, ULB (Brussels), and at the ROCKS Meetings.
ATVA, ADHS, CAV, CDC, Concur, FM, FORTE, Gandalf, HVC, ICALP, iFM, MMB, PSI, QEST, SafeComp.
FMSD, J.Systems and Software, JCST, STTT
I co-organised the 1st and 2nd UnRAVEL Spring Meetings.
- Tom Janson, Accelerated Model Repair using Heuristic Analysis of Subsystems (BSc, RWTH)
- Tim Quatmann, Multi-Objective Model Checking for Markov Automata (MSc, RWTH)
- Ronja Nocon, Pattern-based detection of Monotonicity in Dynamic Fault Trees (BSc, RWTH) – together with Matthias Volk
- Michael Deutschen, GSPN Semantics for Dynamic Fault Trees (MSc, RWTH) – together with Matthias Volk
- Dustin Jungen, Repairs in Dynamic Fault Trees (BSc, RWTH) – together with Matthias Volk
- Sebastian Kruse, Model Checking a Wireless Token-Passing Network (MSc, RWTH)
- Sven Deserno, Model Checking Families of Markov Chains (MSc, RWTH) – together with Benjamin Kaminski
- Jip Spel, Monotonicity in Markov Chains (MSc, RWTH)
- Dustin Jungen, SAT-Based Methods for Solving POMDP problems (MSc, RWTH)
- Kevin Batz, Probabilistic IC3 (MSc, RWTH) – together with Benjamin Kaminski and Christoph Matheja
- Model Checking (RWTH, Winter 2019)
- Datastructures and Algorithms (RWTH, Summer 2018)
- Concurrency Theory (RWTH, Winter 2017)
- Compiler Construction (RWTH, Summer 2017)
- Introduction to Model Checking (RWTH, Summer 2016)
- Modeling and Verification of Probabilistic Systems (RWTH, Winter 2015)
- Introduction to Program Analysis (RWTH, Proseminar, Sumer 2019)
- Trends and Pearls of Model Checking (RWTH, Seminar, Winter 2019)
- Formal Verification Meets Machine Learning (RWTH, Seminar, Summer 2018)
- Programming Language Design and Implementation (RWTH, Seminar, Winter 2017)
- Introduction to Program Analysis (RWTH, Proseminar, Winter 2016)
- Probabilistic Programming (RWTH, Seminar, Summer 2016)
- Algorithms and Data Structures (RWTH, Proseminar, Winter 2015)
- Introduction to probabilistic model checking (UC Berkeley, Formal Methods, 2020)
- On parameter synthesis (RWTH, Modeling and Verification of Probabilistic Systems, 2019)