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

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

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

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