Nils Jansen

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 lookhere. My publications as seen by DBLP are**here. Find my Google Scholar profilehere**. 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

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.

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”

Publications