Moves News

Katoen named ACM Fellow

Prof. Joost-Pieter Katoen has been named ACM Fellow 2020 for his contributions to model checking of software and probabilistic systems. The ACM Fellows program recognizes the top 1% of ACM Members for their outstanding accomplishments in computing and information technology and/or outstanding service to ACM and the larger computing community. Fellows are nominated by their […]

5 Gold medals at RERS 2020

We are happy to announce that our team (Joshua Moerman and Jana Berger) has won 5 gold medals at the RERS challenge 2020. By using a combination of off-the-shelf verification tools, they have managed to crack many of the reachability problems and LTL verification problems. To get more information, please read their report.

Three papers at TACAS 2021

We are delighted to inform you that three MOVES papers have been accepted at TACAS 2021: “Inductive Synthesis for Probabilistic Programs Reaches New Horizons” by Roman Andriushchenko, Milan Ceska, Sebastian Junges and Joost-Pieter Katoen “Multi-objective Optimization of Long-run Average and Total Rewards” by Tim Quatmann and Joost-Pieter Katoen, and “Finding Provably Optimal Markov Chains” by Jip […]

Paper at ESOP 2021

The paper entitled “Automated Termination Analysis of Polynomial Probabilistic Programs ” by Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen and Laura Kovács has been accepted for the European Symposium on Programming (ESOP 2021). The paper presents an algebraic approach and the publicly available tool Amber to automatically prove whether a probabilistic programs is almost-surely terminating (or […]

Distinguished POPL 2021 Paper Award

We are happy to announce that the paper A Pre-Expectation Calculus for Probabilistic Sensitivity by Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Kaminski, Joost-Pieter Katoen and Christoph Matheja has been selected as distinguished POPL 2021 paper. The paper develops a logic for estimating sensitivity properties (how do changes in the inputs affect the program’s output?) […]

LOPSTR 2020 Best Paper Award

We are happy to announce that the paper “Generating Functions for Probabilistic Programs” by Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman and Tobias Winkler has received the best paper award at LOPSTR 2020, the 30th Int. Symp. on Logic-Based Program Synthesis and Transformation.

Job Opportunities as Student Assistants

We are seeking two talented student assistants to support the digitalisation of online bridging courses in Theoretical Computer Science. More concretely, the following tasks need to be performed: the development and implementation of generators for exercise tasks and Moodle plugins and the creation of new and the preparation of existing learning material in Moodle. More […]

Thesis Awards

During the virtual Tag der Informatik, two students of our group have been awarded for their final theses. Florian Keßler received the CS Department Award for his bachelor’s thesis On the Decidability of Entailment Checking in Quantitative Separation Logics, while Jan Svejda received the DSA Industrial Award for his master’s thesis entitled Interpretation-Based Violation Witness Validator. Congratulations!

Book Foundations of Probabilistic Programming Published

The book “Foundations of Probabilistic Programming”, edited by Gilles Barthe, Joost-Pieter Katoen and Alexandra Silva has been published under gold open access. It contains survey chapters of various leading researchers on formal semantics, verification, analysis and applications of probabilistic programming. Get your free download at:

ICT Young Researcher Award

On October 30, the ICT Young Researcher Award 2020 has been awarded to Christopher Brix, who did his master thesis entitled Proving Non-Existence of Imperceptible Adversarial Examples in Deep Neural Networks Using Symbolic Propagation With Error Bounds in our group. The award is given to students at Bachelor, Master and Ph.D. level at RWTH Aachen […]