ECOOP 2025
Mon 30 June - Fri 4 July 2025 Bergen, Norway
Fri 4 Jul 2025 15:00 - 15:30 at M208 - Afternoon session Chair(s): Davide Ancona

Not all properties are monitorable. This is a well-known fact, and it means there exist properties that cannot be fully verified at runtime. However, given a non-monitorable property, a monitor can still be synthesised, but it could end up in a state where no verdict will ever be concluded on the satisfaction (resp., violation) of the property. For this reason, non-monitorable properties are usually discarded. In this work, we carry out an in-depth analysis on monitorability, and how non-monitorable properties can still be partially verified. We present our theoretical results at a semantic level, without focusing on a specific formalism. Then, we show how our theory can be applied to achieve partial runtime verification of linear time properties expressed by concrete formalisms such as LTL.

Ain’t No Stopping Us Monitoring Now - Slides (Ain’t No Stopping Us Monitoring Now.pdf)176KiB

Fri 4 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:45
Afternoon sessionVORTEX at M208
Chair(s): Davide Ancona DIBRIS, University of Genova, Italy
14:00
60m
Keynote
Tell Me The Future, Correctly: On The Monitorability of Timed Logics Over Infinite Executions
VORTEX
K: Mohammed Aristide Foughali Université Paris Cité / IRIF
15:00
30m
Talk
Ain’t No Stopping Us Monitoring Now (extended abstract)
VORTEX
Luca Ciccone University of Turin, Francesco Dagnino , Angelo Ferrando University of Modena and Reggio Emilia
File Attached