Joost-Pieter Katoen

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:

Ackermann Award 2020

Benjamin Kaminski will receive the prestigious 2020 Ackermann Award for his Ph.D. dissertation on “Advanced Weakest Precondition Calculi for Probabilistic Programs” which he defended in February 2019. The Ackermann Award is an annual award by the EACSL (European Association of Computer Science Logic) and is given to an outstanding dissertation in the area “Logic in […]

Storm Journal Paper

The paper ” The Probabilistic Model Checker Storm” by Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann and Matthias Volk has been accepted for the Journal of Software Tools in Technology Transfer. The paper presents the ins and outs of Storm, the model checker for discrete and continuous Markov models (with and without non-determinism) that […]

Two POPL 2021 Papers

We are delighted to announce that the following papers have been accepted for ACM Principles of Programming Languages 2021: ┬áRelatively Complete Verification of Probabilistic Programs by Kevin Batz, Benjamin Kaminski, Joost-Pieter Katoen and Christoph Matheja, and A Pre-Expectation Calculus for Probabilistic Sensitivity by Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Kaminski, Joost-Pieter Katoen and Christoph […]

3rd Place TRA VISIONS 2020 Young Researcher Competition

Congratulations to Matthias Volk and Norman Weik who got the 3rd place in the Young Researcher Competition in the Category “Rail” for their contribution “Reliability analysis of railway station infrastructure based on dynamic fault trees” at the TRA VISIONS 2020 Conference, see

Paper at LOPSTR 2020

The paper entitled “Generating Functions for Probabilistic Programs” by Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman and Tobias Winkler has been accepted for presentation at the 30th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR). The paper presents a denotational semantics for probabilistic programs using generator functions, shows it relation […]

Paper at ATVA 2020

The paper entitled “Verification of indefinite-horizon POMDPs” by Alexander Bork, Sebastian Junges (UC Berkeley), Joost-Pieter Katoen and Tim Quatmann has been accepted for the 18th Int. Symp. on Automated Technology for Verification and Analysis (ATVA 2020). The key idea is to use abstractions of belief states and apply an abstraction-refinement strategy to verify unbounded reachability […]

Two papers at QEST 2020

The papers entitled “Bayesian Inference by Symbolic Model Checking” by Bahare Salmani and Joost-Pieter Katoen and “Probabilistic Model Checking of AODV” by Mojgan Kamali and Joost-Pieter Katen have been accepted at the 17th Int. Conf. on Quantitative Evaluation of Systems (QEST 2020). Out of 42 submissions to QEST 2020, 10 papers have been unconditionally accepted […]

Paper in JAR

The paper entitled “Multi-Cost Bounded Trade-off Analysis in MDP” by Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen and Tim Quatmann has been accepted for the Journal of Automated Reasoning. The paper presents a memory-efficient algorithm for multi-objective model checking problems on Markov decision processes (MDPs) with multiple cost structures.

Paper at EDCC 2020

The paper entitled “Explaining Boolean-logic Driven Markov Processes using GSPNs” authored by Shahid Khan, Joost-Pieter Katoen and Marc Bouissou (EDF) has been accepted for the European Dependable Computing Conference (EDCC 2020). The paper presents a modular semantics of BDMPs using generalised stochastic Petri nets. Transition priorities are used to resolve possible non-deterministic error propagation.