Nils Jansen

nils 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.

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 herediss_cover

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.

I was an external reviewer for, amongst others, CAV, TACAS, Theoretical Computer Science, CONCUR, Petri Nets, VMCAI, FSTTCS, QEST, FORMATS, ATVA, FORMATS, HSCC, TASE, FMOODS-FORTE, and FACS.


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.

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.

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”