The research paper “Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families” by Sebastian Junges, Luko van der Maas (both Radboud University, Nijmegen), Milan Ceska, Filip Macák (both Brno University of Technology), and Tim Quatmann (RWTH) has been accepted for CAV 2026. The paper introduces a practically efficient method to compute optimal conditional […]

The tool paper “Caesar: A Deductive Verifier for Probabilistic Programs” by Philipp Schröer, Kevin Batz, Umut Yiğit Dural, Darion Haase, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja has been accepted for presentation at the 38th International Conference on Computer Aided Verification (CAV 2026), to be held in Lisbon, Portugal. The paper reports on five […]

The paper entitled “Verifying STL Properties of Sliding-Window Neural Classifiers under Adversarial Perturbations” by Xaver Fink (CERN+RWTH), Borja Adiego Fernandez (CERN) and Joost-Pieter Katoen has been accepted for presemtation at RExAI 2026 : International Workshop on Formal Requirements Engineering and Artificial Intelligence. This paper considers the problem of robustness verification (using STL) for neural network […]

The paper “Adversarial Robustness of Time-Series Classification for Crystal Collimator Alignment” by Xaver Fink (RWTH & CERN), Borja Fernandez Adiego, Daniele Mirarchi, Eloise Matheson, Álvaro García González, Gianmarco Ricci (all CERN), Joost-Pieter Katoen has been accepted for presentation at the 18th NASA Formal Methods Symposium (NFM 2026). The paper analyzes and improves the adversarial robustness of a convolutional neural network (CNN) […]

The tutorial “Probabilistic Model Checking Taken by Storm” by Matthias Volk (Eindhoven Univ. of Technology), Linus Heck, Sebastian Junges (Radboud University), Joost-Pieter Katoen, and Tim Quatmann has been accepted for publication and presentation at the Formal Methods 2026 Symposium in Tokyo.

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