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

This program is tentative and subject to change.

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

Shielding has emerged as a promising approach for ensuring safety of AI-controlled autonomous systems. The algorithmic goal is to compute a shield, which is a runtime safety enforcement tool that needs to monitor and intervene the AI controller’s actions if safety could be compromised otherwise. Traditional shields are designed statically for a specific safety requirement. Therefore, if the safety requirement changes at runtime due to changing operating conditions, the shield needs to be recomputed from scratch, causing delays that could be fatal. We introduce dynamic shields for parametric safety specifications, which are succinctly represented sets of all possible safety specifications that may be encountered at runtime. Our dynamic shields are statically designed for a given safety parameter set, and are able to dynamically adapt as the true safety specification (permissible by the parameters) is revealed at runtime. The main algorithmic novelty lies in the dynamic adaptation procedure, which is a simple and fast algorithm that utilizes known features of standard safety shields, like maximal permissiveness. We report experimental results for a robot navigation problem in unknown territories, where the safety specification evolves as new obstacles are discovered at runtime. In our experiments, the dynamic shields took a few minutes for their offline design, and took between a fraction of a second and a few seconds for online adaptation at each step, whereas the brute-force online recomputation approach was up to 5 times slower.

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