From November 18 to 20, 2025, the MISSION Project was represented at the Space Tech Expo Europe in Bremen, Germany—Europe’s largest B2B space event. Our project partners D3TN and Osmium each hosted a booth, showcasing their latest developments and highlighting MISSION’s contributions to the design of reliable and efficient next-generation spacecraft. Two short presentations about the MISSION Project were also given […]

The paper “Diagnostics in Probabilistic Program Verification” by Philipp Schröer, Darion Haase, and Joost-Pieter Katoen has been accepted at the Dafny 2026 workshop. The paper focuses on effective user diagnostics generated during the deductive verification of probabilistic programs. It is based on providing different kinds of program slices for (1) error reporting, (2) proof simplification, […]

The paper “Search and Explore: Symbiotic Policy Synthesis in POMDPs” by Roman Andruishchenko (Brno University of Technology), Alexander Bork, Milan Češka (Brno University of Technology), Sebastian Junges (Radboud University), Joost-Pieter Katoen, and Filip Macák (Brno University of Technology) has been accepted in Formal Methods in System Design (Special Issue CAV 2023). The paper presents a […]

The paper “Weighted Automata for Exact Inference in Discrete Probabilistic Programs” by Dominik Geißler (TU Berlin) and Tobias Winkler has been accepted for presentation at ICTAC 2025. The paper explores the use of weighted automata for performing inference in probabilistic programs over integer variables.

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