September 14, 2026
The paper “Probabilistic Programming Meets Automata Theory: Exact Inference using Weighted Automata” by Dominik Geißler (TU Berlin) and Tobias Winkler has been accepted for publication in Theoretical Computer Science. The paper introduces probability generating automata (PGA), a class of weighted automata used to encode distributions over nonnegative integers.
Read more about Paper in Theoretical Computer ScienceJuly 2, 2026
The paper “Approximately Compatible Graph Predicates: Verifying Program Termination using Graph Grammars” by Alexander Ferber, Ira Fesefeldt, Thomas Noll and Emmett Rayes has received the EATCS Best Paper Award at the 19th International Conference on Graph Transformation (ICGT 2026) in Rennes, France.
Read more about EATCS Best Paper AwardJune 11, 2026
We are pleased to announce that the MOVES group at RWTH Aachen University, together with the University of Twente, will organize CAV 2027, the 39th International Conference on Computer-Aided Verification, in Amsterdam, The Netherlands. CAV is the flagship conference in the field of automated verification. The 2027 edition will take place from July 19–23, 2027, at KIT in Amsterdam and will be the first CAV edition held in the Netherlands. The conference website is now online:…
Read more about CAV 2027 in AmsterdamJune 5, 2026
The paper “Verifying Sampling Algorithms via Distributional Invariants” by Daniel Zilken, Kevin Batz, Joost-Pueter Katoen and Tobias Winkler has won the Best Paper Award at the Formal Methods Symposium 2026 in Tokyo! 🎉🇯🇵. Discrete samplers are to probabilistic computing what arithmetic is for classical programs — powering randomised algorithms, cryptography, AI planning, probabilistic inference, and simulation. But how to prove them correct? Exactly. The key idea: treat probabilistic…
Read more about Best paper award at FM 2026May 4, 2026
The paper “Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops” by Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Kaminski (Saarland Univ.), Joost-Pieter Katoen, Lutz Klinkenberg and Tobias Winkler received the Distinguished Artefact Award at ETAPS 2026 in Turin.
May 4, 2026
The paper entitled “On Termination of Polynomial Programs with Equality Conditions” by Yangjia Li (ISCAS), Mingshuai Chen (Zhejiang Univ.), Liangran Zhao (Peking Univ.), Naijun Zhan (Peking Univ.), Hui Lu (Nanjing), Guohua Wu (Nanyang Univ.), and Joost-Pieter Katoen has been accepted for publication in the journal Information and Computation. The paper provides a decidability result for the termination problem on a wide class of multi-path polynomial programs (MPPs) which were proposed more…
Read more about Paper in Information and ComputationApril 21, 2026
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 reachability probabilities in MDPs. On acyclic MDPs, the approach decides in linear time, whether the conditional…
Read more about Paper at CAV 2026April 20, 2026
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 years of development of Caesar, a deductive verifier for probabilistic programs. Compared to the earlier OOPSLA 2023…
Read more about Tool Paper at CAV 2026April 7, 2026
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 classifiers that operate on time-series data via sliding windows.
March 15, 2026
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) that assists crystal-collimator alignment at the…
Read more about Paper at NFM 2026March 10, 2026
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.
February 12, 2026
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.
February 12, 2026
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 with probabilistic ATL objectives under partial observability.
February 8, 2026
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 (MDPs) via a process of over- and under-approximation that converges towards sound results. (2) Verifying…
Read more about 1-2-3 Papers at Formal Methods 2026December 22, 2025
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 Markov Decision Processes, specifically addressing the achievability question: does there exist a strategy that meets a given set of objectives?