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.
.jpg){kind=link}