Joost-Pieter Katoen

Paper at OOPSLA 2024

The paper entitled “Exact Bayesian Inference for Loopy Probabilistic Programs Using Generating Functions” by Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase and Joost-Pieter Katoen has been accepted for the Conference Object-Oriented Programming, Systems, Languages, and Applications 2024 (OOPSLA). The paper presents a novel exact inference technique for discrete probabilistic programs with unbounded loops and conditioning. […]

Nomination for ETAPS 2024 Best Paper Award

The paper “Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains” by Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler has been nominated for one of the ETAPS 2024 best paper awards. (For Tim, this is the second year in a row to be nominated for such an award.)

ERC Proof-of-Concept Granted

The ERC has granted the Proof-of-Concept proposal VERIPROB (A Deductive Verifier for Probabilistic Programs) by Joost-Pieter Katoen. The grant will enables the further development of Caesar, a verifier vor weakest precondition-reasoning on probabilistic programs.

Two Papers at TACAS 2024

The papers “Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains” by Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler and “Learning Explainable and Better Performing Representations of POMDP Strategies” by Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretinsky and Stefanie Mohr have both been accepted at TACAS 2024 in Luxemburg. The […]

Paper at AAAI 2024

The paper entitled “Natural Strategic Ability in Stochastic Multi-Agent Systems” by Raphael Berthon, Monyque Myttelmann, Antoniello Murano and Joost-Pieter Katoen has been accepted for the 38th AAAI Conference on Artificial Intelligence (AAAI 2024) in Vancouver, Canada. The paper present complexity result on the model checking of the probabilistic alternating temporal logics PATL and PATL∗ under […]

Tim Quatmann wins a KI-Starter Grant

Tim Quatmann has been awarded a KI-Starter Grant for his project proposal “Verifying AI Systems under Partial Observability“. The KI-Starter Grant is an initiative of the State North-Rhine Westphalia to strengthen its position in AI and in particular stimulates young researchers in their academic career. Tim’s project focuses on the automated verification using model checking […]

Paper at POPL 2024

The paper entitled “Programmatic Strategy Synthesis: Resolving Nondeterminism in  Probabilistic Programs” by Kevin Batz, Tom Biskup, Joost-Pieter Katoen, and Tobias Winkler has been accepted at the 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024). The paper shows how to use deductive verification to resolve pure nondeterminism in probabilistic programs such that the obtained determinized program […]

Paper in LMCS Journal

The paper entitled “Model Checking Temporal Properties of Recursive Probabilistic Programs” by Tobias Winkler, Christina Gehnen and Joost-Pieter Katoen has been accepted for the special issues devoted to FoSSaCS 2022 in the journal Logical Methods in Computer Science. The paper shows that model checking a probabilistic pushdown automata against omega visibly push-down languages (e.g., expressed […]

Distinguished Artifact at OOPSLA 2023

The paper “A Deductive Verification Infrastructure for Probabilistic Programs” by Philipp Schröer, Kevin Batz, Benjamin Kaminski, Joost-Pieter Katoen and Christoph Matheja received a distinguished artifact award at OOPSLA 2023. The artifact consists of the deductive verifier Caesar together with a couple of benchmark examples. Caesar has a website at where the tool can be […]

Paper in FMSD Journal

The paper entitled “Parameter Synthesis for Markov Models” by Sebastian Junges, Erika Abraham, Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk has been accepted for publication in the journal Formal Methods in System Design. The paper gives a comprehensive overview of several synthesis problems on parametric Markov chains and MDPs, presents algorithms […]