| Monday Sept. 15 |
Tuesday Sept. 16 |
Wednesday Sept. 17 |
Thursday Sept. 18 |
Friday Sept. 19 |
|
|---|---|---|---|---|---|
| 09:00 – 10:00 | 9:00 Workshops Session 1 |
9:00 Keynote by Thomas Henzinger Algorithmic Fairness: A Runtime Perspective |
9:00 Keynote by Nils Jansen Neurosymbolic Learning Systems: Artificial Intelligence and Formal Methods |
9:00 Keynote by Ankush Desai Gain Confidence in System Correctness using Formal and Semi-formal Methods |
9:00 Keynote by Daniela Micucci Human Activity Recognition with Inertial Data: Approaches and Challenges |
| 10:00 – 10:30 | 10:00 Coffee break |
10:00 Coffee break |
10:00 Coffee break |
10:00 Coffee break |
10:00 Coffee break |
| 10:30 – 10:55 | 10:30 Workshops Session 2 |
10:30 Session 1: Logics and Formalisms |
10:30 Session 4: Machine Learning |
10:30 Session 5: Stream RV |
10:30 Session 8: Anomaly Detection |
| 10:55 – 11:20 | |||||
| 11:20 – 11:45 | |||||
| 11:45 – 12:10 | |||||
| 12:10 – 13:30 | 12:10 Lunch break |
12:10 Lunch break |
12:10 Lunch break |
12:10 Lunch break |
12:10 Lunch break |
| 13:30 – 13:55 | 13:30 Workshops Session 3 |
13:30 Session 2: Probabilistic Systems |
13:30 Social Event Visit of the Riegersburg bird of prey observatory (sponsored by ISEC) |
13:30 Session 6: CPS and Robtics |
13:30 Session 9: Distributed Systems and Hyperproperties |
| 13:55 – 14:20 | |||||
| 14:20 – 14:45 | |||||
| 14:45 – 15:15 | 14:45 Coffee break |
14:45 Coffee break |
14:45 Coffee break |
14:45 Goodbye coffee break |
|
| 15:15 – 15:45 | 15:15 Workshops Session 4 |
15:15 Tutorial: DSLs for Runtime Verification |
15:15 Test-of-Time Award Presentation |
||
| 15:45 – 17:30 | 15:45 Tool Demos & Cocktails |
||||
| 16:15 – 16:45 | |||||
| 17:00 – 17:30 |
Proceedings
You can access the conference proceedings for free via this link provided by Springer Nature.
Monday, September 15
8:15 to 9:00
Registration & Welcome
8:15
Registration
9:00 to 10:00
Workshop Session 1
Session 1 of the workshops RVmeetsMBD, RVCase, and VASSAL
10:30 to 12:10
Workshop Session 2
Session 2 of the workshops RVmeetsMBD, RVCase, and VASSAL
12:10 to 13:30
Lunch break
13:30 to 14:45
Workshop Session 3
Session 3 of the workshops RVmeetsMBD, RVCase, and VASSAL
15:15 to 16:45
Workshop Session 4
Session 4 of the workshops RVmeetsMBD, RVCase, and VASSAL
Tuesday, September 16
8:15 to 9:00
Registration & Welcome
8:15
Registration
8:50
Introduction to RV25
Bettina Könighofer, Hazem Torfah
9:00 to 10:00
Keynote by Thomas Henzinger
10:30 to 12:10
Session 1: Logics and Formalisms
Session Chair
Bernd Finkbeiner
10:30
Modular and Online Monitoring of Temporal Logic Specification with Integral and Filter
by Simone Silvetti, Laura Nenzi, Michele Loreti
10:55
Instrumenting Runtime Enforcement
by François Hublet, David Basin, Linda Hu, Srdjan Krstic, Lennard Reese
11:20
Runtime Consultants
by Dana Fisman, Elina Sudit
11:45
Execution and monitoring of HOA automata with HOAX
by Luca Di Stefano
12:10 to 13:30
Lunch break
13:30 to 14:45
Session 2: Probabilistic Systems
Session Chair
Chih-Hong Cheng
13:30
Runtime Verification for LTL in Stochastic Systems
by Javier Esparza, Vincent Fischer
13:55
Alignment Monitoring
by Konstantin Kueffner, Thomas Henzinger, I Sun, Vasu Singh
14:20
Conformal Safety Shielding for Imperfect-Perception Agents
by William Scarbro, Calum Imrie, Sinem Getir Yaman, Kavan Fatehi, Corina Pasareanu, Radu Calinescu, Ravi Mangal
15:15 to 16:45
Session 3: Tutorial
15:15
DSLs for Runtime Verification
by Klaus Havelund, Doron Peled
Wednesday, September 17
9:00 to 10:00
Keynote by Nils Jansen
Neurosymbolic Learning Systems: Artificial Intelligence and Formal Methods
10:30 to 12:10
Session 4: Machine Learning
Session Chair
Laura Nenzi
10:30
Formal Verification of Neural Certificates Done Dynamically
by Thomas Henzinger, Konstantin Kueffner, Emily Yu
10:55
Statistical Runtime Verification for LLMs via Robustness Estimation
by Natan Levy, Adiel Ashrov, Guy Katz
11:20
Runtime Monitoring and Enforcement of Conditional Fairness in Generative AIs
by Chih-Hong Cheng, Changshun Wu, Xingyu Zhao, Saddek Bensalem, Harald Ruess
11:45
The Power of Reframing: Using LLMs in Synthesizing RV Monitors
by Itay Cohen, Doron Peled, Klaus Havelund, Yoav Goldberg
12:10 to 13:30
Lunch break
13:30 to 22:00
Social Event: Riegersburg castle & Buschenschank dinner
We will depart from the conference venue at 13:30 for an excursion to Riegersburg Castle, located east of Graz. There, we will visit the bird of prey observatory (sponsored by ISEC, TU Graz), where we will enjoy a live demonstration featuring various birds of prey.
Following the visit, we will head to a traditional Buschenschank, a Styrian wine tavern, to enjoy a relaxed evening with regional specialties. The menu will feature locally sourced cold cuts, traditional Styrian fare, and a selection of local beverages.
To complement the Styrian specialties, the event will include scientific lightning talks and the announcement of the winners of the RV25 Best Paper Awards and the RV25 Test of Time Award; a celebration of both recent advances and long-lasting contributions to research, providing a basis for engaging scientific discussions.
Bus transfers to and from the conference venue are available for all participants.
Thursday, September 18
9:00 to 10:00
Keynote by Ankush Desai
Gain Confidence in System Correctness using Formal and Semi-formal Methods
10:30 to 12:10
Session 5: Stream RV
Session Chair
Masaki Waga
10:30
Active Monitoring with RTLola: A Specification-Guided Scheduling Approach
by Jan Baumeister, Bernd Finkbeiner, Frederik Scheerer
10:55
DynSRV: Dynamically Updated Properties for Stream Runtime Verification
by Morten Haahr Kristensen, Thomas Wright, Cláudio Gomes, Lukas Esterle, Peter Gorm Larsen
11:20
A Practical Approach to Runtime Verification
by Raik Hipler, Hannes Kallwies, Martin Leucker, Kevin Gillian van Dommele, Jannis Wien
11:45
A ROS Adapter for RTLola
by Jan Baumeister, Bernd Finkbeiner, Franz Jünger, Florian Kohn, Sebastian Schirmer, Christoph Torens
12:10 to 13:30
Lunch break
13:30 to 14:45
Session 6: CPS and Robotics
Session Chair
Marek Chalupa
13:30
A Compositional Approach to Diagnosing Faults in Cyber-Physical Systems
by Josefine Graebener, Inigo Incer, Richard Murray
13:55
Extended Timed Regular Expressions
by Marco Muniz, Marius Mikučionis, Kim Guldstrand Larsen
14:20
Monitoring Progress and Failure in Autonomous Robot Navigation: A Case Study
by Vladislav Nenchev, Prodromos Sotiriadis
15:15 to 16:45
Session 7: Test of Time Award & Tool Demo Session
15:15
Test-of-Time Award presentation
15:45
Tool Demo with Cocktails
Tools:
- DynSRV: a Stream Runtime Verification language that allows for dynamic updates of properties without losing the internal state.
Presenters: Morten Haahr Kristensen, Thomas Wright - Kairos: a runtime verification tool for distributed systems that monitors Past-Based Temporal Logic (PBTL) properties over partial order executions.
Presenters: Moran Omer, Doron Peled, Ely Porat, and Vijay K. Garg - PoET: a runtime verification tool for concurrent and distributed systems.
Presenters: Moran Omer, Doron Peled, Ely Porat, and Vijay K. Garg - SyMon: Monitor for properties parametric in both time and data
Presenter: Masaki Waga - LLMon: an interactive research tool for describing temporal requirements in plain English – and get runnable runtime-verification (RV) monitors back.
Presenters: Itay Cohen, Klaus Havelund, Doron Peled, and Yoav Goldberg - HOApp: a prototype tool implementing several useful operations on these automata, including product, emptiness checking, and translation of LTL with predicates into the new format
Presenter: Luca Di Stefano - Quint: Quint has been battle-tested in projects such as Malachite, MonadBFT, Neutron, and many more.
Presenter: Ivan Gavran - RTLola: A framework for real-time stream-based monitoring.
Presenter: Frederik Scheerer - RVHyno: a tool for generating monitors for hypernode logic and hypernode automata specifications.
Presenter: Marek Chalupa - EnfGuard: a runtime enforcement tool that enforces Metric First-Order Temporal Logic (MFOTL) specifications in real-time.
Presenter: François Hublet - MODD+Scenic: A framework for generating runtime monitors for operational design domains of AI-based autonomous systems.
Presenters: Alejandro Luque Cerpa, Antonina Skurka
Friday, September 19
9:00 to 10:00
Keynote by Daniela Micucci
Human Activity Recognition with Inertial Data: Approaches and Challenges
10:30 to 12:10
Session 8: Anomaly Detection
Session Chair
Martin Tappler
10:30
Conformal Predictive Monitoring for Multi-Modal Scenarios
by Francesca Cairoli, Luca Bortolussi, Jyotirmoy Deshmukh, Lars Lindemann, Nicola Paoletti
10:55
Hidden-Layer Monitoring for Out-of-Distribution Localization in Image Segmentation
by Jan Kretinsky, Sabine Rieder, Gesina Schwalbe, Youssef Shoeb
11:20
CoCAI: Copula-based Conformal Anomaly Identification for Multivariate Time-Series
by Nicholas Andrea Pearson, Francesca Zanello, Davide Russo, Luca Bortolussi, Francesca Cairoli
11:45
ISL: Monitoring Image Segmentation Logic in Medical Imaging Analysis
by Ziyan An, Daniel Moyer, Ipek Oguz, Taylor T. Johnson, Meiyi Ma
12:10 to 13:30
Lunch break
13:30 to 14:45
Session 9: Distributed Systems and Hyperproperties
Session Chair
Francesca Cairoli
13:30
Monitoring Distributed Systems based on Partial Order Executions with Global States
by Moran Omer, Doron Peled, Porat Ely, Vijay Garg
13:55
Hyper pattern matching
by Masaki Waga, Étienne André
14:20
Monitoring Hypernode Logic Over Infinite Domains
by Marek Chalupa, Thomas Henzinger, Ana Oliveira da Costa