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

This program is tentative and subject to change.

You're viewing the program in a time zone which is different from your device's time zone change time zone

Mon 27 Oct

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

09:30 - 10:30
NIER 1NIER at R102
09:30
30m
Talk
Regular Theories and How to Decide Them
NIER
Umang Mathur National University of Singapore, Singapore
10:00
30m
Talk
Controller Synthesis for Reactive Systems with Communication Delay by Formula Translation
NIER
Sajiv Kumar J.S. , Raghavan Komondoor Indian Institute of Science
11:00 - 12:30
NIER 2NIER at R102
11:00
30m
Talk
Property Grouping and Context-Aware Runtime Enforcement
NIER
Saumya Shankar International Institute of Information Technology Bangalore, Srinivas Pinisetty Indian Institute of Technology Bhubaneswar, Thierry Jéron INRIA
11:30
30m
Talk
Compositional Probabilistic Model Checking with String Diagrams of MDPs 
NIER
Ichiro Hasuo National Institute of Informatics, Japan
12:00
30m
Talk
PhantomDrive: A Privacy-Focused Navigation System for Concealing User Movements
NIER
Inzemamul Haque Indian Institute of Technology Kanpur, Pankaj Siwan , Indranil Saha IIT Kanpur
14:00 - 14:30
NIER 3NIER at R102
14:00
30m
Talk
Bidding Your Way to Better Decisions
NIER
Guy Avni University of Haifa, Kaushik Mallik IST Austria, Austria, Suman Sadhukhan
14:30 - 15:30
Tutorial 1ATutorials and Workshops at R102
Chair(s): Raghavan Komondoor Indian Institute of Science
14:30
60m
Tutorial
Replicated Data Types
Tutorials and Workshops
Kartik Nagar IIT Madras
16:00 - 17:00
16:00
60m
Tutorial
Replicated Data Types
Tutorials and Workshops
Kartik Nagar IIT Madras

Tue 28 Oct

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

09:30 - 10:30
Invited Talk 1Invited Talks at Amantran
Chair(s): Alex Potanin Australian National University

(Joint APLAS-ATVA Invited Talk)

09:30
60m
Talk
15 Years of Viper: Building and Evolving a Verification Infrastructure (Joint APLAS-ATVA Invited Talk)
Invited Talks
Peter Müller ETH Zurich
11:00 - 12:30
AutomataATVA Papers at R102
Chair(s): Srinivas Pinisetty Indian Institute of Technology Bhubaneswar
11:00
30m
Paper
Componentwise Automata Learning for System IntegrationDistinguished Paper
ATVA Papers
Hiroya Fujinami , Masaki Waga Kyoto University, Jie An Institute of Software Chinese Academy of Sciences, Kohei Suenaga Graduate School of Informatics, Kyoto University, Hiroki Iseri NPO ASTER Minato-ku, Tokyo, Ichiro Hasuo National Institute of Informatics, Japan
11:30
30m
Paper
Learning Event-recording Automata Passively
ATVA Papers
Sayan Mukherjee Univ Rennes, Inria, CNRS, IRISA, France, Jean-François Raskin Université Libre de Bruxelles
12:00
15m
Paper
[TOOL] TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets (tool paper)
ATVA Papers
Peter Gjøl Jensen Aalborg University, Denmark, Jiri Srba , Martin Zimmermann University of Liverpool
11:00 - 12:30
Type Systems, Safety, and VerificationAPLAS Papers at R104
11:00
30m
Paper
Memory Safety: Uniqueness as Separation
APLAS Papers
Pilar Selene Linares Arévalo University of Melbourne, Arthur Azevedo de Amorim Rochester Institute of Technology, USA, Vincent Jackson University of Melbourne, Liam O'Connor Australian National University, Peter Schachte The University of Melbourne, Christine Rizkallah University of Melbourne
11:30
30m
Paper
Fair Termination for Resource-Aware Active Objects
APLAS Papers
Francesco Dagnino , Paola Giannini University of Eastern Piedmont, Violet Ka I Pun Western Norway University of Applied Sciences, Ulises Torrella Høgskulen på Vestlandet
12:00
30m
Paper
A Formal Foundation for Equational Reasoning on Probabilistic Programs
APLAS Papers
Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Japan, Yoshihiro Ishiguro , Zachary Stone The MathComp-Analysis development team
14:00 - 15:30
Verification IATVA Papers at R102
Chair(s): Kartik Nagar IIT Madras
14:00
30m
Paper
Data Structures for Finite Downsets of Natural Vectors: Theory and Practice
ATVA Papers
Michaël Cadilhac , Guillermo A. Perez University of Antwerp
14:30
30m
Paper
Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains
ATVA Papers
Linus Heck RWTH Aachen University, Tim Quatmann RWTH Aachen University, Jip Spel RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University, Sebastian Junges RWTH Aachen University, Germany
15:00
30m
Paper
Antarbhukti: Verifying Correctness of PLC Software during System Evolution
ATVA Papers
Soumyadip Bandyopadhyay ABB Corporate Research Center, India, Santonu Sarkar BITS Pilani, India
14:00 - 15:30
Control, Effects, and DecidabilityAPLAS Papers at R104
14:00
30m
Paper
Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers
APLAS Papers
Ryunosuke Endo Waseda University, Tachio Terauchi Waseda University
14:30
30m
Paper
Expressive Power of One-Shot Control Operators and Coroutines
APLAS Papers
Kentaro Kobayashi Department of Computer Science, University of Tsukuba, Yukiyoshi Kameyama University of Tsukuba
15:00
30m
Paper
Positive Sharing and Abstract Machines
APLAS Papers
Beniamino Accattoli Inria & Ecole Polytechnique, Claudio Sacerdoti Coen University of Bologna, Jui-Hsuan Wu CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668
16:00 - 17:30
Hybrid and Dynamical SystemsATVA Papers at R102
16:00
30m
Paper
Control Closure Certificates
ATVA Papers
16:30
30m
Paper
Deriving Liveness Properties of Hybrid Systems from Reachable Sets and Lyapunov-like Certificates
ATVA Papers

17:00
15m
Paper
[TOOL] Evaluation, Reduction, and Approximation of Dynamical Systems and Networks with ERODE
ATVA Papers
Luca Cardelli Microsoft Research and University of Oxford, Giuseppe Squillace , Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy, Max Tschaikowski IMT Institute for Advanced Studies Lucca, Italy, Andrea Vandin DTU, Denmark
16:00 - 17:00
Quantum Programming and LogicAPLAS Papers at R104
16:00
30m
Paper
IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation
APLAS Papers
Kinnari Dave Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles, Alejandro Díaz-Caro INRIA / LORIA & UNQ, Vladimir Zamdzhiev Inria
16:30
30m
Paper
A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
APLAS Papers
Alejandro Díaz-Caro INRIA / LORIA & UNQ, Nicolas A. Monzon Universidad de la República & Universidad Argentina de la Empresa

Wed 29 Oct

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

09:30 - 10:30
Invited Talk 2Invited Talks at Amantran
09:30
60m
Talk
Network Abstractions for Modularity and Performance Verification
Invited Talks
Aarti Gupta Princeton University
11:00 - 12:30
GamesATVA Papers at R102
Chair(s): Sayan Mukherjee Univ Rennes, Inria, CNRS, IRISA, France
11:00
30m
Paper
Energy Games with Weight Uncertainty
ATVA Papers
Orna Kupferman Hebrew University
11:30
30m
Paper
Quantitative Strategy Templates
ATVA Papers
Satya Prakash Nayak Max Planck Institute for Software Systems (MPI-SWS), Ritam Raha University of Antwerp, Antwerp, Belgium, Irmak Saglam Max Planck Institute for Software Systems (MPI-SWS), Anne-Kathrin Schmuck Max Planck Institute for Software Systems
12:00
30m
Paper
Widest Path Games and Maximality Inheritance in Bounded Value Iteration for Stochastic Games
ATVA Papers
Kittiphon Phalakarn National Institute of Informatics, Ichiro Hasuo National Institute of Informatics, Japan
11:00 - 12:30
Program Analysis, Specifications, and Decision ProceduresAPLAS Papers at R104
11:00
30m
Paper
Checking Consistency of Event-driven Traces
APLAS Papers
Parosh Aziz Abdulla Uppsala University; Mälardalen University, Mohamed Faouzi Atig Uppsala University, Sweden, Samuel Grahn Uppsala University, Govind Rajanbabu Uppsala University, Ramanathan S. Thinniyam Uppsala University
11:30
30m
Paper
Specification Inference modulo Oracles for Database-backed Web Applications
APLAS Papers
12:00
30m
Paper
Decision Procedures for A Theory of String Sequences
APLAS Papers
Denghang Hu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Taolue Chen Birkbeck, University of London, Philipp Ruemmer University of Regensburg and Uppsala University, Fu Song Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences; Nanjing Institute of Software Technology, Zhilin Wu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
14:00 - 15:30
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
Kaushik Mallik IST Austria, Austria, César Sánchez IMDEA Software Institute
14:30
30m
Paper
Learning Verified Monitors for Hidden Markov Models
ATVA Papers
Luko van der Maas , Sebastian Junges RWTH Aachen University, Germany
15:00
30m
Paper
Prompt Runtime Enforcement
ATVA Papers
Ayush Anand Indian Institute of Technology Bhubaneswar, Thierry Jéron INRIA, Sayan Mukherjee Univ Rennes, Inria, CNRS, IRISA, France, Srinivas Pinisetty Indian Institute of Technology Bhubaneswar
14:00 - 15:00
AI and Compiler Optimisation for PerformanceAPLAS Papers at R104
14:00
30m
Paper
ELTC: An End-to-End Large Language Model-Based Tensor Compilation Optimization Framework
APLAS Papers
wenbo ma Tiangong University, qingzeng song Tiangong University, yongjiang xue Tiangong University, Fei Qiao Tsinghua University, mingze sun Tiangong University
14:30
30m
Paper
Performance Optimization of HPC Workloads in Cloud Using AI-Driven Algorithms
APLAS Papers
15:00 - 16:00
APLAS SRC 1APLAS Papers at R104

Thu 30 Oct

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

09:30 - 10:30
Invited Talk 3Invited Talks at Amantran
09:30
60m
Talk
LLMs meet Program Synthesis
Invited Talks
Rahul Sharma Microsoft Research
11:00 - 12:30
LearningATVA Papers at R102
Chair(s): Kittiphon Phalakarn National Institute of Informatics
11:00
30m
Paper
Inductive Generalization in Reinforcement Learning from Specifications
ATVA Papers
Vignesh Subramanian , Subhajit Roy IIT Kanpur, Suguman Bansal Georgia Institute of Technology, USA
11:30
30m
Paper
Locally Pareto-Optimal Interpretations for Black-Box Machine Learning Models
ATVA Papers
Supratik Chakraborty IIT Bombay, S. Akshay , Hazem Torfah Chalmers University of Technology
12:00
30m
Paper
Solution-aware vs global ReLU selection: partial MILP strikes back for DNN verification
ATVA Papers
Blaise Genest IPAL - CNRS - CNRS@CREATE, Kuldeep S. Meel National University of Singapore
11:00 - 12:30
APLAS SRC 2APLAS Papers at R104
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
Sayan Mitra University of Illinois at Urbana-Champaign, Ivan Ruchkin University of Florida
14:30
15m
Paper
[Tool] PolyQEnt: A Polynomial Quantified Entailment SolverDistinguished Tool Paper
ATVA Papers
Krishnendu Chatterjee IST Austria, Amir Kafshdar Goharshady University of Oxford, Ehsan Kafshdar Goharshady , Mehrdad Karrabi , Đorđe Žikelić Singapore Management University, Singapore
14:45
15m
Paper
[TOOL] Q-Sylvan: A Parallel Decision Diagram Package for Quantum Computing
ATVA Papers
Sebastiaan Brand , Alfons Laarman Leiden University
14:00 - 15:00
APLAS SRC 3APLAS Papers at R104
15:00 - 16:00
Tutorial 2ATutorials and Workshops at R102
Chair(s): B Srivathsan Chennai Mathematical Institute
15:00
60m
Tutorial
Quantitative and Probabilistic Verification
Tutorials and Workshops
Benjamin Lucien Kaminski Saarland University; University College London
16:30 - 17:30
16:30
60m
Tutorial
Quantitative and Probabilistic Verification
Tutorials and Workshops
Benjamin Lucien Kaminski Saarland University; University College London

Fri 31 Oct

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

09:30 - 10:25
09:30
55m
Talk
Talk 1
Tutorials and Workshops
Ahmed Bouajjani IRIF, Université Paris Diderot
11:00 - 12:55
11:00
55m
Talk
Talk 2: Causally Deterministic (factored) Markov Decision Processes.
Tutorials and Workshops
12:00
55m
Talk
Talk 3
Tutorials and Workshops
Pavithra Prabhakar Kansas State University
16:00 - 17:00
MMAC Workshop 4: Milestones and MotifsTutorials and Workshops at Amantran