The Program, and Accepted papers can be viewed in the respective tabs. For more details see Papers page of APLAS.
Dates
Tracks
Plenary
This program is tentative and subject to change.
Mon 27 OctDisplayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
Mon 27 Oct
Displayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
08:30 - 09:30 | |||
08:30 60mRegistration | ATVA/APLAS Registration Invited Talks | ||
Tue 28 OctDisplayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
Tue 28 Oct
Displayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
08:30 - 09:15 | |||
08:30 45mRegistration | ATVA/APLAS Registration Invited Talks | ||
09:15 - 09:30 | |||
09:15 15mDay opening | Opening Remarks Invited Talks | ||
09:30 - 10:30 | Invited Talk 1Invited Talks at Amantran Chair(s): Alex Potanin Australian National University (Joint APLAS-ATVA Invited Talk) | ||
09:30 60mTalk | 15 Years of Viper: Building and Evolving a Verification Infrastructure (Joint APLAS-ATVA Invited Talk) Invited Talks Peter Müller ETH Zurich | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Coffee Break Catering | ||
11:00 - 12:30 | |||
11:00 30mPaper | 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, Nayuta Yanagisawa , Hiroki Iseri NPO ASTER Minato-ku, Tokyo, Ichiro Hasuo National Institute of Informatics, Japan | ||
11:30 30mPaper | Learning Event-recording Automata Passively ATVA Papers Anirban Majumdar , Sayan Mukherjee Univ Rennes, Inria, CNRS, IRISA, France, Jean-François Raskin Université Libre de Bruxelles | ||
12:00 15mPaper | TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets (tool paper) ATVA Papers Bruno Maria René Gonzalez TU Berlin, Germany, Peter Gjøl Jensen Aalborg University, Denmark, Jiri Srba , Stefan Schmid TU Berlin, Germany, Martin Zimmermann University of Liverpool | ||
11:00 - 12:30 | Type Systems, Safety, and VerificationAPLAS Papers at R104 Chair(s): Alex Potanin Australian National University | ||
11:00 30mPaper | 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 30mPaper | 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 30mPaper | 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 | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 30mPaper | Data Structures for Finite Downsets of Natural Vectors: Theory and Practice ATVA Papers Michaël Cadilhac , Vanessa Fluegel University of Antwerp, Antwerp, Belgium, Guillermo A. Perez University of Antwerp, Shrisha Rao University of Antwerp, Antwerp, Belgium | ||
14:30 30mPaper | Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains ATVA Papers Linus Heck Radboud University, Tim Quatmann RWTH Aachen University, Jip Spel RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University, Sebastian Junges Radboud University | ||
15:00 30mPaper | Antarbhukti: Verifying Correctness of PLC Software during System Evolution ATVA Papers Pre-print | ||
14:00 - 15:30 | Control, Effects, and DecidabilityAPLAS Papers at R104 Chair(s): Sanjiva Prasad Indian Institute of Technology Delhi | ||
14:00 30mPaper | Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers APLAS Papers | ||
14:30 30mPaper | Expressive Power of One-Shot Control Operators and Coroutines APLAS Papers | ||
15:00 30mPaper | 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 | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Coffee Break Catering | ||
16:00 - 17:30 | |||
16:00 30mPaper | Control Closure Certificates ATVA Papers Vishnu Murali University of Colorado Boulder, Mohammed Adib Oumer University of Colorado Boulder, Majid Zamani | ||
16:30 30mPaper | Deriving Liveness Properties of Hybrid Systems from Reachable Sets and Lyapunov-like Certificates ATVA Papers | ||
17:00 15mPaper | Evaluation, Reduction, and Approximation of Dynamical Systems and Networks with ERODE (tool paper) 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 Chair(s): Alex Potanin Australian National University | ||
16:00 30mPaper | 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 30mPaper | 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 OctDisplayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
Wed 29 Oct
Displayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
09:30 - 10:30 | Invited Talk 2Invited Talks at Amantran Chair(s): Meenakshi D'Souza IIITB - International Institute of Information Technology Bangalore | ||
09:30 60mTalk | Network Abstractions for Modularity and Performance Verification Invited Talks Aarti Gupta Princeton University | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Coffee Break Catering | ||
11:00 - 12:30 | |||
11:00 30mPaper | Energy Games with Weight Uncertainty ATVA Papers | ||
11:30 30mPaper | Quantitative Strategy Templates ATVA Papers Ashwani Anand Max Planck Institute for Software Systems, 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 30mPaper | Widest Path Games and Maximality Inheritance in Bounded Value Iteration for Stochastic Games ATVA Papers Kittiphon Phalakarn National Institute of Informatics, Yun Chen Tsai National Institute of Informatics, Japan, Ichiro Hasuo National Institute of Informatics, Japan | ||
11:00 - 12:30 | Program Analysis, Specifications, and Decision ProceduresAPLAS Papers at R104 Chair(s): PRITAM MANOHAR GHARAT Microsoft Research India | ||
11:00 30mPaper | 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 30mPaper | Specification Inference modulo Oracles for Database-backed Web Applications APLAS Papers | ||
12:00 30mPaper | 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 | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | Monitoring and Runtime VerificationATVA Papers at R102 Chair(s): Ichiro Hasuo National Institute of Informatics, Japan | ||
14:00 30mPaper | 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 30mPaper | Learning Verified Monitors for Hidden Markov Models ATVA Papers | ||
15:00 30mPaper | 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 | ||
14:00 - 15:00 | AI and Compiler Optimisation for PerformanceAPLAS Papers at R104 Chair(s): Meenakshi D'Souza IIITB - International Institute of Information Technology Bangalore | ||
14:00 30mPaper | 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 30mPaper | Performance Optimization of HPC Workloads in Cloud Using AI-Driven Algorithms APLAS Papers | ||
15:00 - 16:00 | |||
16:00 - 16:30 | |||
16:00 30mCoffee break | Coffee Break Catering | ||
16:30 - 19:00 | |||
16:30 2h30mBreak | Excursion Catering | ||
Thu 30 OctDisplayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
Thu 30 Oct
Displayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
09:30 - 10:30 | |||
09:30 60mTalk | LLMs meet Program Synthesis Invited Talks Rahul Sharma Microsoft Research | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Coffee Break Catering | ||
11:00 - 12:30 | |||
11:00 30mPaper | Inductive Generalization in Reinforcement Learning from Specifications ATVA Papers Vignesh Subramanian , Rohit Kushwah , Subhajit Roy IIT Kanpur, Suguman Bansal Georgia Institute of Technology, USA | ||
11:30 30mPaper | Locally Pareto-Optimal Interpretations for Black-Box Machine Learning Models ATVA Papers Aniruddha Joshi UC Berkeley, Supratik Chakraborty IIT Bombay, S. Akshay , Shetal Shah IIT Bombay, India, Hazem Torfah Chalmers University of Technology, Sanjit Seshia UC Berkeley | ||
12:00 30mPaper | Solution-aware vs global ReLU selection: partial MILP strikes back for DNN verification ATVA Papers Yuke Liao CNRS@CREATE, Singapore, Blaise Genest IPAL - CNRS - CNRS@CREATE, Kuldeep S. Meel National University of Singapore, Shaan Aryaman NYU | ||
11:00 - 12:30 | |||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:00 | |||
14:00 30mPaper | 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 15mPaper | 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 15mPaper | Q-Sylvan: A Parallel Decision Diagram Package for Quantum Computing (tool paper) ATVA Papers | ||
14:00 - 15:00 | |||
16:00 - 16:30 | |||
16:00 30mCoffee break | Coffee Break Catering | ||