ATVA 2025
Mon 27 - Fri 31 October 2025 Bengaluru, India

This program is tentative and subject to change.

Wed 29 Oct 2025 15:00 - 15:30 at R102 - Monitoring and Runtime Verification Chair(s): Ichiro Hasuo

This paper deals with the problem of runtime enforcement (RE) in the context of reactive systems, which consists in modifying the outputs of a system minimally to ensure its correctness. In contrast to enforcers that can postpone events via buffering, enforcers for reactive systems must operate within the same reactive cycle, always yielding a (possibly modified) output. For safety properties, an enforcer makes sure to satisfy the property at each step. However, for general regular properties, one can only expect to satisfy the property eventually. There is then a risk that even under enforcement the satisfaction is indefinitely delayed, and the property is never actually satisfied. Forcing the satisfaction of regular or $\omega$-regular properties has been considered using bounded fairness and prompt eventuality. In this paper, we propose a new runtime enforcement framework for regular properties with prompt eventualities. Given an automaton specifying a property $\varphi$ and a bound $k$, the enforcer should never falsify $\varphi$ more than $k$ consecutive steps. We formally define this RE problem, characterize $k$-enforceability of automata, and exhibit the construction of the enforcer. Rather than fixing $k$, we also study whether $k$ can be computed to ensure $k$-enforceability or some maximal coverage of $\varphi$. We implement the $k$-prompt enforcement framework, and demonstrate its behaviour with varying $k$.

This program is tentative and subject to change.

Wed 29 Oct

Displayed time zone: Chennai, Kolkata, Mumbai, New Delhi change

14:00 - 15:30
Monitoring and Runtime VerificationATVA Papers at R102
Chair(s): Ichiro Hasuo National Institute of Informatics, Japan
14:00
30m
Paper
Efficient Dynamic Shielding for Parametric Safety Specifications
ATVA Papers
Davide Corsi University of California, Irvine, Kaushik Mallik IST Austria, Austria, Andoni Rodríguez IMDEA Software Institute, Spain, César Sánchez IMDEA Software Institute
14:30
30m
Paper
Learning Verified Monitors for Hidden Markov Models
ATVA Papers
Luko van der Maas Radboud University Nijmegen, Netherlands, Sebastian Junges Radboud University
15:00
30m
Paper
Prompt Runtime Enforcement
ATVA Papers
Ayush Anand Indian Institute of Technology Bhubaneswar, Loïc Germerie Guizouarn University of Rennes, France / Inria, France / CNRS, France / IRISA, France, Thierry Jéron INRIA, Sayan Mukherjee Univ Rennes, Inria, CNRS, IRISA, France, Srinivas Pinisetty Indian Institute of Technology Bhubaneswar, Ocan Sankur University of Rennes, France / Inria, France / CNRS, France / IRISA, France
Hide past events