The paper entitled “Verification of Robust Multi-Agent Systems” by Raphael Berthon, Munyque Myttelmann, (CNRS, LIPN, Sorbonne Paris North University) Joost-Pieter Katoen and Nello Morano (University of Napels) has been accepted for presentation at the 25th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2026). This paper investigates robust verification strategies for stochastic multi‑agent systems […]

From January 23 to 30, the MOVES Group organised the 10th edition of its famous Söllerhaus Workshop at Hirschegg in Kleinwalsertal, Austria. Again, it was a very successful event, full of research talks, discussions, and (a little bit of) skiing.

The following three papers have been accepted for the 27th Symposium on Formal Methods (2026) in Tokyo, Japan: (1) Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking by Arnd Hartmanns (U. Twente), Tim Quatmann and Mark van Wijk (U. Twente). This paper introduces tools for approximating multi-objective probabilistic model checking for Markov decision processes […]

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 “Towards safe and robust neural network controllers at CERN: a review of methods and challenges” by Xaver Fink, Borja Fernandez Adiego (CERN), Brad Schofield (CERN) and Joost-Pieter Katoen has been accepted at the 20th International Conference on Accelerator and Large Experimental Physics Control Systems (ICALEPCS’25, https://proceedings.jacow.org/icalepcs2025/). The paper reviews the challenges of ensuring […]

The two papers “Verifying Sampling Algorithms via Distributional Invariants” by Kevin Batz (University College London), Joost-Pieter Katoen, Tobias Winkler and Daniel Zilken and “Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops” by Kevin Batz (University College London), Adrian Gallus, Darion Haase, Benjamin Kaminski (Saarland University and University College London), Joost-Pieter Katoen, Lutz Klinkenberg […]

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