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

The paper “The Dial-a-Ride Problem in Primary Care with Flexible Scheduling” by Felix Engelhardt, Emma Ahrens, Christina Büsing together with Felix Rauh from University Leuven has been accepted for publication in the journal OR Spektrum. The paper generalizes the Dial-A-Ride problem, which models the transportation of patients in a rural area, such that it differentiates between chronic […]

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).