image by Herbert Frank, CC BY 2.0

 ROCKS Workshop 2023

 ROCKS Workshop 2023

ROCKS: Rigorous dependability analysis using model checking techniques for stochastic systems

The 2023 ROCKS workshop will take place in September 2023 at Saarland University in Saarbrücken, Germany.



Preliminary programme, subject to change.

The workshop's programme consists of a keynote by Joël Ouaknine on Thursday (indicated by a "K" in the schedule below) as well as long talks (of approx. 20 minutes, indicated by an "L"), medium-length talks (of approx. 10 minutes, indicated by an "M"), and short talks (of approx. 5 minutes, indicated by an "S") by participants from the ROCKS community.

All regular sessions take place in Hörsaal 001 on the ground floor of Building E1 3.

Wednesday, September 27
10:30 – 11:00 Coffee Break
11:00 – 12:30 Session W1 (Session Chair: Benjamin Kaminski)
Introduction and Welcome
L Property Specification and Models for Risk: Towards Risk Propagation Graphs
Stefano M. Nicoletti (University of Twente)
M Fast Verified SCCs for Probabilistic Model Checking
Bram Kohlen (University of Twente)
M The SAFEST tool for fault tree analysis
Matthias Volk (University of Twente)
M Programmatic Strategy Synthesis
Tobias Winkler (RWTH Aachen University)
S Rusty Fault Trees
Andreas Schmidt (Universität des Saarlandes)
12:30 – 14:00 Lunch at AC
14:00 – 15:00 Session W2 (Session Chair: Christoph Matheja)
L Algebraic Analysis of Probabilistic Loops
Marcel Moosbrugger (Technische Universität Wien)
M Partial Incorrectness Logic
Lena Verscht (Universität des Saarlandes)
M Bi-Objective Lexicographic Optimization
Debraj Chakraborty (Masaryk University)
15:00 – 15:30 Coffee Break
15:30 – 17:30 Session W3 (Session Chair: Kevin Batz)
L Probabilistic Hyperproperties
Lina Gerlach (RWTH Aachen University)
M Matrix-based Inference in Discrete-time Markov Models
Nikolai Käfer (Technische Universität Dresden)
M Exact Bayesian Inference using PGF
Lutz Klinkenberg (RWTH Aachen University)
M Partially Observable Environments with Active Measuring
Merlijn Krale (Radboud University)
M Fuzzy Quantitative Attack Tree Analysis
Nhung Dang (University of Twente)
S Entropic Risk for Turn-Based Stochastic Games
Jakob Piribauer (Technische Universität München)
Thursday, September 28
09:26 – 10:30 Session T1 (Session Chair: Holger Hermanns)
K Keynote
Joël Ouaknine (Max Planck Institute for Software Systems)
M Probabilistic Belief Programming
Tobias Gürtler (Universität des Saarlandes)
10:30 – 11:00 Coffee Break
11:00 – 12:30 Session T2 (Session Chair: Sebastian Junges)
M Termination Analysis of Simple Randomised Linear Loops
Eleanore Meyer (RWTH Aachen University)
M Proving Almost-Sure Termination of Probabilistic Programs Using Term Rewriting
Jan-Cristoph Kassing (RWTH Aachen University)
M Efficient Sensitivity Analysis for Parametric Robust Markov Chains
Thom Badings (Radboud University)
M Certificates for Multi-Objective Queries in Markov Decision Processes
Calvin Chau (Technische Universität Dresden)
M Verifying Multi-Environment MDPs
Marck van der Vegt (Radboud University)
M OxiDD: A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in Rust
Nils Husung (Universität des Saarlandes)
S How To Play If You Cannot Win?
Mariëlle Stoelinga (University of Twente)
12:30 – 14:00 Lunch at AC
14:00 – 15:00 Session T3 (Session Chair: Thom Badings)
L Comparing Two Approaches to Include Stochasticity in Hybrid Automata
Lisa Willemsen (University of Twente)
M Optimal Observability in POMDPs
Alyzia Konsta (Technical University of Denmark)
S Uncertainty Assumptions in Robust POMDPs
Eline Bovy (Radboud University)
15:00 – 15:30 Coffee Break
15:30 – 17:00 Session T4 (Session Chair: Joost-Pieter Katoen)
L RealySt: A Tool for Stochastic Hybrid Systems
Jonas Stübbe (Universität Münster)
M Offline Reinforcement Learning with Reliability Guarantees
Marnix Suilen (Radboud University)
M Reinforcement Learning with Formal Guarantees
Patrick Wienhöft (Technische Universität Dresden)
M Partially Explainable Decisions
Jan Křetínský (Technische Universität München)
S Computing Responsibility in Transition Systems
Johannes Lehmann (Technische Universität Dresden)
S Binary Classifiers in Markov Decision Processes
Robin Ziemeck (Technische Universität Dresden)
19:00 Dinner at Stiefel
Friday, September 29
09:00 – 10:30 Session F1 (Session Chair: Arnd Hartmanns)
L ROCKS, Paper, Caesar – Deductive Verification of Probabilistic Programs
Philipp Schroer (RWTH Aachen University)
M MULTIGAIN 2.0: MDP Controller Synthesis for Multiple Mean-Payoff, LTL and Steady-State Constraints
Alexandros Evangelidis (Technische Universität München)
M Relating Approximate Probabilistic Bisimulations
Timm Spork (Technische Universität Dresden)
L Probabilistic Analysis of Control Systems Failures
Martina Maggio (Universität des Saarlandes)
M Safe Integration of Learning in SystemC using Timed Contracts and Model Checking
Pauline Blohm (Universität Münster)
10:30 – 11:00 Coffee Break
11:00 – 12:30 Session F2 (Session Chair: Benjamin Kaminski)
L Matching Distributions under Structural Constraints
Aaron Bies (Universität des Saarlandes)
M Precision Guarantees for Solving Stochastic Games with Value Iteration
Maximilian Weininger (Institute of Science and Technology Austria)
M Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Kevin Batz (RWTH Aachen University)
M Abstraction-Refinement for Hierarchical Probabilistic Models
Sebastian Junges (Radboud University)
M Quantitative Analysis of Safety-Security Interaction
Reza Soltani (University of Twente)
12:30 – 14:00 Lunch at AC


Saarland Informatics Campus is easy to reach by car via motorways A1 from the north, A6 from the east, and French A4/A320 from the south and west. The parking lot Uni Ost (max. 3 €/day) is next to the workshop venue. By train, Saarbrücken Hbf can be reached by high-speed ICE trains running between Frankfurt and Paris as well as by regional trains from Frankfurt via Mainz, from Koblenz via Trier, from Mannheim, and from Metz. From the station, city buses on multiple lines run to Campus; get off at the Universität Mensa bus stop. The local Airport Saarbrücken (SCN) has flights to/from Berlin, Hamburg, and various holiday destinations. It is connected to the city centre by buses running roughly every 60 minutes (approx. 25 minutes travel time), but there is no direct public transport link between the airport and Campus.

Previous ROCKS