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

This program is tentative and subject to change.

Thu 30 Oct 2025 14:00 - 14:30 at R102 - Verification II Chair(s): Ahmed Bouajjani

Precise and comprehensive situational awareness is a critical capability of modern autonomous systems. Deep neural networks that perceive task-critical details from rich sensory signals have become ubiquitous; however, their black-box behavior and sensitivity to environmental uncertainty and distribution shifts make them challenging to verify formally. Abstraction-based verification techniques for vision-based autonomy produce safety guarantees contingent on rigid assumptions, such as bounded errors or known unique distributions. Such overly restrictive and inflexible assumptions limit the validity of the guarantees, especially in diverse and uncertain test-time environments. We propose a methodology that unifies the verification models of perception with their offline and online validation. Our methodology leverages interval MDPs and provides a flexible end-to-end guarantee that adapts directly to the out-of-distribution test-time conditions. We evaluate our methodology on a synthetic perception Markov chain with well-defined state estimation distributions and a mountain car benchmark. Our findings reveal that we can guarantee tight yet rigorous bounds on overall system safety.

This program is tentative and subject to change.

Thu 30 Oct

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

14:00 - 15:00
Verification IIATVA Papers at R102
Chair(s): Ahmed Bouajjani IRIF, Université Paris Diderot
14:00
30m
Paper
Towards Unified Probabilistic Verification and Validation of Vision based Autonomy
ATVA Papers
Jordan Peper University of Florida, USA, Yan Miao University of Illinois Urbana-Champaign, Sayan Mitra University of Illinois at Urbana-Champaign, Ivan Ruchkin University of Florida
14:30
15m
Paper
PolyQEnt: A Polynomial Quantified Entailment Solver (tool paper)Distinguished Tool Paper
ATVA Papers
Krishnendu Chatterjee IST Austria, Amir Kafshdar Goharshady University of Oxford, Ehsan Kafshdar Goharshady , Mehrdad Karrabi , Milad Saadat Sharif University of Technology, Iran, Maximilian Seeliger Vienna University of Technology, Austria, Đorđe Žikelić Singapore Management University, Singapore
14:45
15m
Paper
Q-Sylvan: A Parallel Decision Diagram Package for Quantum Computing (tool paper)
ATVA Papers
Sebastiaan Brand , Alfons Laarman Leiden University
Hide past events