I moved to UT Austin. Find my new webpage here.
I’m a postdoctoral researcher in the MOVES group at RWTH Aachen University, headed by Prof. Dr. Ir. Joost-Pieter Katoen. My research interests include
- verification and (parameter) synthesis for probabilistic systems
- probabilistic programming
- controller synthesis
During my PhD I worked on the generation of counterexamples and their application, symbolic techniques, and the utilization of solving techniques like SAT, SMT or linear programming. Since the beginning of 2014, I am working on probabilistic programs within the APPA project, parameter synthesis for probabilistic/stochastic systems, and recently on probabilistic models for robotic scenarios. Recently, we developed the parametric model checker PROPhESY; the paper was presented at CAV 2015.
Publications
For a list of my publications, technical reports and selected talks please look here. My publications as seen by DBLP are here. Find my Google Scholar profile here. My PhD thesis titled “Counterexamples in Probabilistic Verification” is available at the library webpage and can also be found here. 
Research Projects
I participate(d) in the research projects APPA, CEBug, ROCKS, MEALS and HySmart.
About Me
| 2015 – today | Postdoctoral researcher at RWTH Aachen University |
| 2009 – 2015 | PhD student and research assistant at RWTH Aachen University |
|
2010 – 2014
|
Member of the Commission for Teaching in Computer Science |
| 2010 – 2011 | Member of the AlgoSyn Steering Committee |
| 2002 – 2009 | Studies of computer science at RWTH Aachen University |
| 2001 – 2002 | Civilian services at a small hospital in my hometown |
| 1988 – 2001 | School education |
| 1982 | Born in Simmerath, Germany |
During spring and summer of 2013 as well as spring 2014, I stayed at Universidad Nacional de Cordoba with Pedro R. d’Argenio. Within 2010 – 2013 I’ve stayed many times at the University of Freiburg with Ralf Wimmer and Bernd Becker.
Besides computer science, I’m the conductor of a small orchestra, I enjoy music and reading, and I am very much into food and sometimes sports.
Tools
Recently, we released PROPhESY, a tool for parameter synthesis for probabilistic systems.
Within the CEBug project we have developed the COMICS tool which computes small critical subsystems as counterexamples for Discrete-time Markov Chains. The current version is available on the COMICS-website.
Theses
I have supervised some Bachelor’s or Master’s Theses. Find below the finished ones.
- Lukas Westhofen, “On-the-fly Model Checking for Probabilistic Programs”
- Tim Quatmann, “Counterexamples for Expected Rewards”
- Marian Van de veire, “Minimal Critical Subsystems for Probabilistic Models with Nondeterminism”
- Andreas Vorpahl, “Compositional Counterexamples for MDPs”
- Matthias Volk, “Verification and Synthesis for Parametric Markov Chains”
- Maik Scheffler, “Hierarchical Counterexamples for DTMCs – Case Studies”
- Amith Belur Nagabushana, “Minimal Critical Subsystems for PCTL Properties of Markov Models”