Joost-Pieter Katoen

Photo of Joost-Pieter Katoen

Email: katoen@cs.rwth-aachen.de
Address: Room 4201
Ahornstraße 55
D-52074 Aachen
Phone: +49 241 80 21200

Please visit my personal page in the web

Publications

Own publications

2026

Conference paper
Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler
Programming languages and systems
PDF of Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops RWTH record for Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops BibTeX for Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
Conference paper
Caesar: A Deductive Verifier for Probabilistic Programs
Philipp Schroer, Kevin Batz, Umut Yigit Dural, Darion Haase, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Computer Aided Verification
PDF of Caesar: A Deductive Verifier for Probabilistic Programs RWTH record for Caesar: A Deductive Verifier for Probabilistic Programs BibTeX for Caesar: A Deductive Verifier for Probabilistic Programs
Journal article
Search and explore: symbiotic policy synthesis in POMDPs
Roman Andriushchenko, Alexander Nikolai Bork, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, Filip Macák
Formal methods in system design
PDF of Search and explore: symbiotic policy synthesis in POMDPs RWTH record for Search and explore: symbiotic policy synthesis in POMDPs BibTeX for Search and explore: symbiotic policy synthesis in POMDPs
Conference paper
Verifying Sampling Algorithms via Distributional Invariants
Daniel Zilken, Kevin Batz, Joost-Pieter Katoen, Tobias Winkler
Formal Methods
PDF of Verifying Sampling Algorithms via Distributional Invariants RWTH record for Verifying Sampling Algorithms via Distributional Invariants BibTeX for Verifying Sampling Algorithms via Distributional Invariants
Journal article
On termination of polynomial programs with equality conditions
Yangjia Li, Mingshuai Chen, Liangran Zhao, Naijun Zhan, Hui Lu, Guohua Wu, Joost-Pieter Katoen
Information and computation
RWTH record for On termination of polynomial programs with equality conditions BibTeX for On termination of polynomial programs with equality conditions
Conference paper
Highly Incremental: A Simple Programmatic Approach for Many Objectives
Philipp Schroer, Joost-Pieter Katoen
Formal Methods
PDF of Highly Incremental: A Simple Programmatic Approach for Many Objectives RWTH record for Highly Incremental: A Simple Programmatic Approach for Many Objectives BibTeX for Highly Incremental: A Simple Programmatic Approach for Many Objectives
Preprint
Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)
Philipp Schroer, Joost-Pieter Katoen
PDF of Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)RWTH record for Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)BibTeX for Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)
Conference paper
Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains
Linus Heck, Tim Quatmann, Jip Josephine Spel, Joost-Pieter Katoen, Sebastian Junges
Automated technology for verification and analysis
RWTH record for Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains BibTeX for Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains
Conference paper
Facing Uncertainty in AI: From Formal Verification To Synthesis
Joost-Pieter Katoen
Theoretical Aspects of Computing – ICTAC 2025
RWTH record for Facing Uncertainty in AI: From Formal Verification To Synthesis BibTeX for Facing Uncertainty in AI: From Formal Verification To Synthesis
Book chapter
The Optimal Strategy to Meet the Deadline: Ask Christel!
Joost-Pieter Katoen
Principles of formal quantitative analysis
RWTH record for The Optimal Strategy to Meet the Deadline: Ask Christel!BibTeX for The Optimal Strategy to Meet the Deadline: Ask Christel!
Artifact
Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Artifact Evaluation)
Philipp Schröer, Darion Haase, Joost-Pieter Katoen
Zenodo
RWTH record for Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Artifact Evaluation)BibTeX for Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Artifact Evaluation)

2025

Preprint
Compositional Reasoning for Parametric Probabilistic Automata
Hannah Mertens, Tim Quatmann, Joost-Pieter Katoen
PDF of Compositional Reasoning for Parametric Probabilistic Automata RWTH record for Compositional Reasoning for Parametric Probabilistic Automata BibTeX for Compositional Reasoning for Parametric Probabilistic Automata
Conference paper
Quantifier Elimination and Craig Interpolation: The Quantitative Way
Kevin Batz, Joost-Pieter Katoen, Nora Orhan
Foundations of Software Science and Computation Structures
PDF of Quantifier Elimination and Craig Interpolation: The Quantitative Way RWTH record for Quantifier Elimination and Craig Interpolation: The Quantitative Way BibTeX for Quantifier Elimination and Craig Interpolation: The Quantitative Way
Conference paper
Bayesian Inference in Quantum Programs
Christina Gehnen, Dominique Unruh, Joost-Pieter Katoen
52nd International Colloquium on Automata, Languages, and Programming
PDF of Bayesian Inference in Quantum Programs RWTH record for Bayesian Inference in Quantum Programs BibTeX for Bayesian Inference in Quantum Programs
Preprint
Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
Philipp Schroer, Darion Haase, Joost-Pieter Katoen
PDF of Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)RWTH record for Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)BibTeX for Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
Conference paper
Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Emma Katharina Ahrens, Jan-Christoph Kassing, Jürgen Giesl, Joost-Pieter Katoen
10th International Conference on Formal Structures for Computation and Deduction
PDF of Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems RWTH record for Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems BibTeX for Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Conference paper
A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games
Raphael Jean Berthon, Joost-Pieter Katoen, Zihan Zhou
36th International Conference on Concurrency Theory
PDF of A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games RWTH record for A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games BibTeX for A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games
Conference paper
Compositional Reasoning for Parametric Probabilistic Automata
Hannah Mertens, Tim Quatmann, Joost-Pieter Katoen
36th International Conference on Concurrency Theory
PDF of Compositional Reasoning for Parametric Probabilistic Automata RWTH record for Compositional Reasoning for Parametric Probabilistic Automata BibTeX for Compositional Reasoning for Parametric Probabilistic Automata
Conference paper
Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
Timm Spork, Christel Baier, Joost-Pieter Katoen, Sascha Klüppelholz, Jakob Piribauer
Computer Aided Verification
PDF of Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains RWTH record for Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains BibTeX for Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
Conference paper
Multi-Cost-Bounded Reachability Analysis of POMDPs
Alexander Nikolai Bork, Tim Quatmann, Joost-Pieter Katoen, Svenja Maria Stein
Conference on Uncertainty in Artificial Intelligence, 21-25 July 2025, Rio Othon Palace, Rio de Janeiro, Brazil
PDF of Multi-Cost-Bounded Reachability Analysis of POMDPs RWTH record for Multi-Cost-Bounded Reachability Analysis of POMDPs BibTeX for Multi-Cost-Bounded Reachability Analysis of POMDPs
Conference paper
Robust Strategies for Stochastic Multi-Agent Systems
Raphael Jean Berthon, Joost-Pieter Katoen, Munyque Mittelmann, Aniello Murano
Proceedings of AAMAS-2025
PDF of Robust Strategies for Stochastic Multi-Agent Systems RWTH record for Robust Strategies for Stochastic Multi-Agent Systems BibTeX for Robust Strategies for Stochastic Multi-Agent Systems
Journal article
Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate
Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler
Journal of automated reasoning
PDF of Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate RWTH record for Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate BibTeX for Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate
Journal article
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Kevin Batz, Joost-Pieter Katoen, Francesca Randone, Tobias Winkler
Proceedings of the ACM on programming languages
PDF of Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back RWTH record for Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back BibTeX for Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Journal article
Introduction to the Special Collection from FM 2023
Marsha Chechik, Joost-Pieter Katoen
Formal aspects of computing
RWTH record for Introduction to the Special Collection from FM 2023 BibTeX for Introduction to the Special Collection from FM 2023
Journal article
An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty
Roman Andriushchenko, Milan Češka, Filip Macák, Sebastian Junges, Joost-Pieter Katoen
Journal of artificial intelligence research
PDF of An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty RWTH record for An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty BibTeX for An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty

Supervised theses

2026

Bachelor’s thesis
Belief-tracking policies for partially observable MDPs via randomized finite-state controllers
Ole Dannemeyer
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Tim Quatmann
Consultants: Tobias Winkler, Lisa Pühl
RWTH record for Belief-tracking policies for partially observable MDPs via randomized finite-state controllers BibTeX for Belief-tracking policies for partially observable MDPs via randomized finite-state controllers
Bachelor’s thesis
Distribution transformers for probabilistic programs: a study of inductive definability
Felix Euting
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Daniel Johannes Zilken
RWTH record for Distribution transformers for probabilistic programs: a study of inductive definability BibTeX for Distribution transformers for probabilistic programs: a study of inductive definability
Bachelor’s thesis
Semantic equivalences of probabilistic programs and their underlying Markov chains
Philip Strüwer
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Tim Quatmann
Consultants: Daniel Johannes Zilken, Jan-Gustav Michnia
RWTH record for Semantic equivalences of probabilistic programs and their underlying Markov chains BibTeX for Semantic equivalences of probabilistic programs and their underlying Markov chains
Bachelor’s thesis
Predicate transformers for nondeterministic quantum programs
Xi Wang
RWTH Aachen University
Advisers: Dominique Unruh, Joost-Pieter Katoen
Consultants: Christina Gehnen
PDF of Predicate transformers for nondeterministic quantum programs RWTH record for Predicate transformers for nondeterministic quantum programs BibTeX for Predicate transformers for nondeterministic quantum programs
Master’s thesis
A formal language for expressing quantum predicates
Umut Yigit Dural
RWTH Aachen University
Advisers: Dominique Unruh, Joost-Pieter Katoen
Consultants: Christina Gehnen
PDF of A formal language for expressing quantum predicates RWTH record for A formal language for expressing quantum predicates BibTeX for A formal language for expressing quantum predicates
Master’s thesis
Bounds for quantum weakest preconditions
Jonas Deutsch
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Dominique Unruh
Consultants: Christina Gehnen
PDF of Bounds for quantum weakest preconditions RWTH record for Bounds for quantum weakest preconditions BibTeX for Bounds for quantum weakest preconditions
Master’s thesis
Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning
Jonas Seidel
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Daniel Johannes Zilken
PDF of Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning RWTH record for Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning BibTeX for Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning
Bachelor’s thesis
Which probabalistic programs are modelcheckable?
Samuel Akinlaja
Rheinisch-Westfälische Technische Hochschule Aachen
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Daniel Johannes Zilken
RWTH record for Which probabalistic programs are modelcheckable?BibTeX for Which probabalistic programs are modelcheckable?

2025

PhD thesis
Deductive reasoning about concurrent probabilistic programs
Ira Justus Fesefeldt
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Lars Birkedal
PDF of Deductive reasoning about concurrent probabilistic programs RWTH record for Deductive reasoning about concurrent probabilistic programs BibTeX for Deductive reasoning about concurrent probabilistic programs
Master’s thesis
Multi‐agent path finding for reversible conveyors
Dominic Sebastian Meiser
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Roy Hermanns
PDF of Multi‐agent path finding for reversible conveyors RWTH record for Multi‐agent path finding for reversible conveyors BibTeX for Multi‐agent path finding for reversible conveyors
Bachelor’s thesis
Extending the assume–guarantee framework for parametric probabilistic automata : From robust valuations to the limits of robust strategies
Muhammad Asad Murtaza Butt
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Hannah Mertens
RWTH record for Extending the assume–guarantee framework for parametric probabilistic automata : From robust valuations to the limits of robust strategies BibTeX for Extending the assume–guarantee framework for parametric probabilistic automata : From robust valuations to the limits of robust strategies
Master’s thesis
Cost-reliability optimal spare part allocation in dynamic fault trees with relaxed spare gates
Rico Stanosek
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for Cost-reliability optimal spare part allocation in dynamic fault trees with relaxed spare gates BibTeX for Cost-reliability optimal spare part allocation in dynamic fault trees with relaxed spare gates
Bachelor’s thesis
Scalable qubit routing on the conveyor-based SpinBus architecture
Dobromir Panayotov
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Roy Hermanns
RWTH record for Scalable qubit routing on the conveyor-based SpinBus architecture BibTeX for Scalable qubit routing on the conveyor-based SpinBus architecture
Bachelor’s thesis
Evaluating tool support for fault tree analysis of satellite constellations
Mareike Metzler
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
PDF of Evaluating tool support for fault tree analysis of satellite constellations RWTH record for Evaluating tool support for fault tree analysis of satellite constellations BibTeX for Evaluating tool support for fault tree analysis of satellite constellations
Bachelor’s thesis
Exploration of certificate sharing for neural network verification
Glen Jordan Grant
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix, Xaver Fink
RWTH record for Exploration of certificate sharing for neural network verification BibTeX for Exploration of certificate sharing for neural network verification
Bachelor’s thesis
On the relation of rely-guarantee and assume-guarantee reasoning
Marcel Eissing
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Lena Verscht, Hannah Mertens
PDF of On the relation of rely-guarantee and assume-guarantee reasoning RWTH record for On the relation of rely-guarantee and assume-guarantee reasoning BibTeX for On the relation of rely-guarantee and assume-guarantee reasoning
Bachelor’s thesis
Modeling non-deterministic quantum programs for model checking
Kaleb Kierner
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Dominique Unruh
Consultants: Christina Gehnen
PDF of Modeling non-deterministic quantum programs for model checking RWTH record for Modeling non-deterministic quantum programs for model checking BibTeX for Modeling non-deterministic quantum programs for model checking
Bachelor’s thesis
Implementing the denotational semantics of probabilistic programs
Elbeck Lazaridi
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Daniel Johannes Zilken
RWTH record for Implementing the denotational semantics of probabilistic programs BibTeX for Implementing the denotational semantics of probabilistic programs
PhD thesis
Analysis of probabilistic programs using generating functions
Lutz Klinkenberg
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Laura Kovacs
PDF of Analysis of probabilistic programs using generating functions RWTH record for Analysis of probabilistic programs using generating functions BibTeX for Analysis of probabilistic programs using generating functions
Master’s thesis
Effective quantifier-based reasoning for quantitative deductive verification
Emil Beothy-Elo
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Philipp Schroer, Darion Haase
PDF of Effective quantifier-based reasoning for quantitative deductive verification RWTH record for Effective quantifier-based reasoning for quantitative deductive verification BibTeX for Effective quantifier-based reasoning for quantitative deductive verification
Master’s thesis
Automata-based semantics for the probabilistic programming language ReDiP
Dominik Geißler
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler
PDF of Automata-based semantics for the probabilistic programming language ReDiP RWTH record for Automata-based semantics for the probabilistic programming language ReDiP BibTeX for Automata-based semantics for the probabilistic programming language ReDiP

2024

Master’s thesis
MARVEL: A stepwise debugging tool for Markov models in the PRISM-language
Patrick Arens
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Ira Justus Fesefeldt
RWTH record for MARVEL: A stepwise debugging tool for Markov models in the PRISM-language BibTeX for MARVEL: A stepwise debugging tool for Markov models in the PRISM-language
Bachelor’s thesis
Transfer of branching heuristics for neural network verification to alpha-beta-CROWN and evaluation of large-scale verification benchmarks
Yejun Tang
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix
RWTH record for Transfer of branching heuristics for neural network verification to alpha-beta-CROWN and evaluation of large-scale verification benchmarks BibTeX for Transfer of branching heuristics for neural network verification to alpha-beta-CROWN and evaluation of large-scale verification benchmarks
PhD thesis
Automated deductive verification of probabilistic programs
Kevin Batz
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Ichiro Hasuo
PDF of Automated deductive verification of probabilistic programs RWTH record for Automated deductive verification of probabilistic programs BibTeX for Automated deductive verification of probabilistic programs
PhD thesis
Probabilistic model checking and parameter tuning for Bayesian networks
Bahare Salmani Barzoki
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Luc de Raedt
PDF of Probabilistic model checking and parameter tuning for Bayesian networks RWTH record for Probabilistic model checking and parameter tuning for Bayesian networks BibTeX for Probabilistic model checking and parameter tuning for Bayesian networks

All records on RWTH Publications