Two papers of the MOVES group have been accepted for the European Symposium on Programming (ESOP) 2026 to be held in Turin, Italy. The paper “Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing” by Philipp Schröer, Darion Haase, and Joost-Pieter Katoen presents novel slicing concepts for probabilistic programs, their formalisation and experimental […]

The paper entitled ““Multiple Long-Run and omega-Regular Objectives in MDPs” by Julius Ide, Joost-Pieter Katoen, Hannah Mertens and Tim Quatmann has been accepted for TACAS 2026, to be held in Turin, Italy. The paper was one of the 56 (out of 190) papers that were accepted and presents presents algorithms for solving multi-objective problems in […]

The paper “Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate” by Hannah Mertens, Tim Quatmann, Tobias Winkler and Joost-Pieter Katoen has been accepted for publication in the Journal of Automated Reasoning. This paper presents several numerical algorithms to compute expected visiting times (aka: occupation times) in DTMCs and CTMCs, and […]

The paper entitled “Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains”by Linus Heck (RU Nijmegen), Tim Quatmann, Jip Spel, Joost-Pieter Katoen and Sebastian Junges (RU Nijmegen) has been accepted for the 23rd International Symposium on Automated Technology for Verification and Analysis (ATVA 2025). This paper advances parameter lifting, a technique to check whether all […]

Two papers of the MOVES group have been accepted at CONCUR 2025, the 36th International Conference on Concurrency Theory. It concerns the papers “Compositional Reasoning for Parametric Probabilistic Automata” by Hannah Mertens, Tim Quatmann, and Joost-Pieter Katoen, as well as “A Direct Reduction from Parity to Simple Stochastic Games” by Raphael Berthon, Joost-Pieter Katoen, and […]

The paper entield “Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems” by Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl and Joost-Pieter Katoen has been accepted for the 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) in Birmingham (UK). This paper introduces a general semantics of the (possibly infinite) reduction sequences of an […]

The paper entitled “Bayesian Inference in Quantum Programs” by Christina Gehnen, Dominique Unruh and Joost-Pieter Katoen has been accepted for presentation at the 52nd EATCS International Colloquium on Automata, Languages, and Programming (ICALP 2025 – Track B). This paper considers postselection in quantum physics (aka: Bayesian conditioning in programs), for quantum while-programs, defines an operational […]

The papers “Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains” by Timm Spork, Christel Baier, Joost-Pieter Katoen, Sascha Klüppelholz, and Jakob Piribauer and “Efficient Probabilistic Model Checking for Relational Reachability” by Lina Gerlach, Tobias Winkler, Erika Ábrahám, Borzoo Bonakdarpour and Sebastian Junges have been accepted at the International Conference on Computer-Aided Verification (CAV) 2025. The first paper […]

The paper entitled “Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back” by Kevin Batz, Joost-Pieter Katoen, Francesca Randone (University of Trieste), and Tobias Winkler has been accepted for the International Conference on Object-Oriented Programming Systems, Languages, and Application (OOPSLA 2025). The paper presents a new technique to formally check […]

The DFG together with the FNRS (Belgium) have granted the project, entitled “Mixing Formal Methods and Learning Techniques for Strategy Synthesis in Partially Observable Markov Decision Processes” for a period of three years. This project is a collaboration with the research group of Jean-Francois Raskin (Universite de Libre Bruxelles).