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 […]

The two papers “What is the Best Algorithm for MDP Model Checking?” by Tim Quatmann and “The Revised Practitioner’s Guide to MDP Model Checking Algorithms” by Arnd Hartmanns (University of Twente), Sebastian Junges (Radboud University), Tim Quatmann, and Maximilian Weininger (TU Munich, IST Austria) have been accepted in the International Journal on Software Tools for […]

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 […]

During the ETAPS 2025 Conference at Hamilton, Canada, Kevin Batz has received the prestigious Doctoral Dissertation Award of the ETAPS Association. His PhD dissertation thesis entitled “Automated Deductive Verification of Probabilistic Programs” was considered a milestone, greatly advancing the state-of the art in automated deductive verification of discrete probabilistic programs.

The paper entitled “Multi-Cost-Bounded Reachability Analysis of POMDPs” by Alexander Bork, Joost-Pieter Katoen, Tim Quatmann and Svenja Stein has been accepted for the 41st Conference on Uncertainty in Artificial Intelligence (UAI 2025) in Rio de Janeiro (BR).The paper presents a general framework to approximate the maximal probability to reach a target while satisfying constraints on […]

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 “Using GPUs And LLMs Can Be Satisfying for Nonlinear Real Arithmetic Problems” by Christopher Brix, Julia Walczak, Nils Lommen and Thomas Noll has been accepted for presentation at the VerifAI Workshop at ICLR 2025. The paper describes how satisfying assignments to quantifier-free NRA problems can be found using GPU acceleration, and how LLMs […]