This website is now outdated. Please visit my new website.

In February 2020, I defended my PhD Thesis titled ‘Parameter Synthesis in Markov Models’ with honours.

I was a PhD student at the Software Modeling and Verification Group between June 2015 and February 2020. From October 2017 until February 2020, I was affiliated with the Research Training Group UnRAVeL.

You can also find me on DBLP and Google Scholar.

Research interests

• Model checking of quantitative (parameterised) systems
• Policy synthesis for variants of partially observable MDPs
• Formal aspects of reliability engineering, in particular fault trees
• SMT-solving for real arithmetic
• Formal modelling of real-world systems

Tool support

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 SMT-solver SMT-RAT (2011 — 2015)
• The arithmetic library carl (2012 — 2015) and its python bindings pycarl (since 2016)
• Compass (2014)
• The Markov Chain Parameter Synthesis Framework PROPhESY (since 2014)
• The Probabilistic Model Checker Storm (since 2014) and its python bindings stormpy (since 2016)

B.Sc or M.Sc theses

I’m always looking forward to work with students. If you’re looking for a thesis in one of the areas above, do not hesitate to contact me! Some ideas are given in our list of open topics.

Previously, I supervised the following theses (chronological order):

• Tom Janson, Accelerated Model Repair using Heuristic Analysis of Subsystems (BSc)
• Tim Quatmann, Multi-Objective Model Checking for Markov Automata (MSc)
• Ronja Nocon, Pattern-based detection of Monotonicity in Dynamic Fault Trees (BSc) [together with Matthias Volk]
• Michael Deutschen, GSPN Semantics for Dynamic Fault Trees (MSc) [together with Matthias Volk]
• Dustin Jungen, Repairs in Dynamic Fault Trees (BSc) [together with Matthias Volk]
• Sebastian Kruse, Model Checking a Wireless Token-Passing Network (MSc)
• Sven Deserno,  Model Checking Families of Markov Chains (MSc) [together with Benjamin Kaminski]
• Jip Spel, Monotonicity in Markov Chains (MSc)

Teaching

I was involved in teaching assistance for the following lectures:

• Datastructures and Algorithms (Summer 2018) 
• Concurrency Theory (Winter 2017)
• Compiler Construction (Summer 2017)
• Introduction to Model Checking (Summer 2016)
• Modeling and Verification of Probabilistic Systems (Winter 2015)

Furthermore, I supervised students in the scope of the following seminars:

• Introduction to Program Analysis (Proseminar, Sumer 2019)
• Trends and Pearls of Model Checking (Seminar, Winter 2019)
• Formal Verification Meets Machine Learning (Seminar, Summer 2018)
• Programming Language Design and Implementation (Seminar, Winter 2017)
• Introduction to Program Analysis (Proseminar, Winter 2016)
• Probabilistic Programming (Seminar, Summer 2016)
• Algorithms and Data Structures (Proseminar, Winter 2015)

Reviewer

I have been PC Member for the Artefact Evaluation of ATVA. 

I have been an external reviewer for the following venues:
ATVA, ADHS, CAV, CDC, FM, FORTE, Gandalf, ICALP, iFM, MMB, HVC, PSI, QEST, SafeComp,

and for the following journals:
FMSD, J.Systems and Software.

Warning: SQLite3::prepare(): Unable to prepare statement: 5, database is locked in /var/www/html/inc/sqlite-access.php on line 428

Fatal error: Uncaught SQLiteAccessException: Could not prepare statement: REPLACE INTO publications (pub_id, type_id, title, year, pages, publisher, institution, arxiv_id, doi_id, fulltext) VALUES (:pub_id, :type_id, :title, :year, :pages, :publisher, :institution, :arxiv_id, :doi_id, :fulltext); in /var/www/html/inc/sqlite-access.php:433 Stack trace: #0 /var/www/html/inc/sqlite-access.php(64): dbAccess->prepare('REPLACE INTO pu...') #1 /var/www/html/inc/sqlite-access.php(45): dbAccess->prepareStmts() #2 /var/www/html/index.php(73): dbAccess->__construct('/var/www/html/d...', 1) #3 {main} thrown in /var/www/html/inc/sqlite-access.php on line 433