ROCKS: Rigorous dependability analysis using model checking techniques for stochastic systems
The 2025 ROCKS Meeting will take place at Eindhoven University of Technology (TU/e) in Eindhoven, The Netherlands. The meeting will consist of the main ROCKS Workshop and a Doctoral Symposium preceding the workshop.
| Wednesday, April 2nd | |
| until 12:00 | Arrival |
| 12:00–13:30 | Lunch |
| 13:30–14:00 | Welcome to ROCKS 2025 |
| 14:00–15:00 | PhD speed dating |
| 15:00–15:45 | Coffee break |
| 15:45–16:15 | PhD speed dating |
| 16:15–17:10 | Talks (Session Chair: Jakob Piribauer) |
| Thom Badings, University of Oxford (15 min) Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates |
|
| Marnix Suilen, University of Antwerpen (15 min) Pessimistic Iterative Planning for Robust POMDPs |
|
| Group Christel Baier, TU Dresden (15 min) Timm Spork – Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains |
|
| Group Jan Křetínský, Masaryk University Brno (10 min) Marta Grobelna – Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games |
|
| from 17:30 | Reception at Zwarte Doos |
| Thursday, April 3rd | |
| 09:00–09:45 | Keynote Sofie Haesaert, Eindhoven University of Technology: Verification and Control of Stochastic Difference Equations |
| 09:45–10:30 | Coffee break |
| 10:30–12:00 | Talks (Session Chair: Marnix Suilen) |
| Group Sebastian Junges, Radboud University Nijmegen (30 min) Loes Kruger – Active Automata Learning with Reference Models Luko van der Maas – Learning Verified Monitors for Hidden Markov Models |
|
| Group Nils Jansen, Ruhr University Bochum (15 min) Eline Bovy – How Sticky is Your Model? Game Semantics for Robust POMDPs Maximilian Weininger – 100 Reasons Why Your Statistical Model Checking is Unsound |
|
| Group Markus Siegle, Universität der Bundeswehr München (15 min) Fabian Michel – Formal Bounds for Transient Distributions of Markov Processes |
|
| Group Anne Remke, Universität Münster (30 min) Jonas Stübbe & Lisa Willemsen – Powering Up Analysis: Tool Support for Battery-Powered Systems |
|
| 12:00–13:30 | Lunch |
| 13:30–15:00 | Talks (Session Chair: Maximilian Weininger) |
| Group Christel Baier, TU Dresden (30 min) Rajab Aghamov – Model Checking Linear Temporal Logic with Standpoint Modalities Johannes Lehmann – Probabilistic Abstraction Refinement Using Witnessing Subsystems |
|
| Group Jan Křetínský, Masaryk University Brno (20 min) Debraj Chakraborty – Explainable Representation of Finite-Memory Policies for POMDPs Kush Grover – Resilient Strategies for Stochastic Systems |
|
| Group Holger Hermanns, Universität des Saarlandes (15 min) Nils Husung – OxiDD-viz: Visualizing Decision Diagrams through OxiDDation (Part 1) |
|
| FSA group, Eindhoven University of Technology (25 min) Tar van Krieken – OxiDD-viz: Visualizing Decision Diagrams through OxiDDation (Part 2) Sebastián Betancourt – Measuring Robustness of an AI Car with Stark |
|
| 15:00–15:45 | Coffee break |
| 15:45–17:30 | Talks (Session Chair: Kevin Batz) |
| Group Christoph Matheja, University of Oldenburg (20 min) Oliver Bøving – Expected Total Costs of Infinite MDPs in Lean Roberto Pettinau – Towards Model Checking Infinite Families of DTMCs Generated by Graph Grammars |
|
| Group Benjamin Kaminski, Universität des Saarlandes (20 min) Anran Wang – Strongest Post Transformer for LTL Tobias Gürtler – Combining Nondeterminism and Conditioning in Probabilistic Programming |
|
| Group Milan Češka, Brno University of Technology (20 min) Milan Češka – Introduction Filip Macák – Policies Grow on Trees: Model Checking Families of MDPs |
|
| Group Joost-Pieter Katoen, RWTH Aachen University (30 min) Daniel Zilken – Fixed Point Certificates for Reachability & Expected Rewards in MDPs Emma Ahrens – A Framework for Online Optimization |
|
| Carlos E. Budde, Technical University of Denmark (15 min) Timed Rare Event Simulation for Repairable Dynamic Fault Trees |
|
| from 19:00 | Workshop dinner at Trafalgar Pub, Dommelstraat 21 |
| Friday, April 4th | |
| 09:00–09:45 | Talks (Session Chair: Stefano Nicoletti) |
| Group Erika Ábrahám, RWTH Aachen University (15 min) Lina Gerlach – Efficient Probabilistic Model Checking for Relational Reachability |
|
| Group Arnd Hartmanns, University of Twente (30 min) Annabell Petri – Formal Models for Critical Water Infrastructure in the North Sea Region: Taming Mölndalsån Mark van Wijk – Multi-Objective Model Checking for Modest Bram Kohlen – Fast Verified Floating-Point Computations for Probabilistic Model Checking |
|
| 09:45–10:30 | Coffee break |
| 10:30–12:00 | Talks (Session Chair: Thom Badings) |
| Group Sebastian Junges, Radboud University Nijmegen (15 min) Linus Heck – Generalized Parameter Lifting for Parametric Markov Chains |
|
| Group Nils Jansen, Ruhr University Bochum (30 min) Maris Galesloot – Robust Finite-Memory Policies for Hidden-Model POMDPs Merlijn Krale – Tighter Value-Function Approximations for POMDPs Joshua Wendland – Missingness in POMDPs Miriam Ackermann – Uncertainty-Aware Perception POMDPs Jule Schmidt – Causal and Safe Reinforcement Learning Matéo Torrents – Resilient Strategies for POMDPs |
|
| Group Marielle Stoelinga, University of Twente (45 min) Benedikt Peterseim – Attack Trees, Compositionally Georgiana Caltais – Racing Bugs in SDN Milan Lopuhaä-Zwakenberg – Analyzing Attack-Fault Trees via MDPs Yanni Dong – Smart System Diagnosis via Fault Trees and Diagnostic Decision Trees |
|
| 12:00–13:30 | Lunch |
The TU/e campus can be reached from Eindhoven train station by foot in less than 10 minutes.
