Filter Program
Dates
Rooms
Tracks
Badges
Your Program
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
09:30 - 10:30 | |||
09:30 30mTalk | Regular Theories and How to Decide Them NIER Umang Mathur National University of Singapore, Singapore | ||
10:00 30mTalk | Controller Synthesis for Reactive Systems with Communication Delay by Formula Translation NIER |
11:00 - 12:30 | |||
11:00 30mTalk | 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 30mTalk | Compositional Probabilistic Model Checking with String Diagrams of MDPs NIER Ichiro Hasuo National Institute of Informatics, Japan | ||
12:00 30mTalk | PhantomDrive: A Privacy-Focused Navigation System for Concealing User Movements NIER |
14:00 - 14:30 | |||
14:00 30mTalk | Bidding Your Way to Better Decisions NIER |
14:30 - 15:30 | |||
14:30 60mTutorial | Replicated Data Types Tutorials and Workshops Kartik Nagar IIT Madras |
16:00 - 17:00 | |||
16:00 60mTutorial | Replicated Data Types Tutorials and Workshops Kartik Nagar IIT Madras |
Tue 28 OctDisplayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
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 60mTalk | 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 | |||
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, Hiroki Iseri NPO ASTER Minato-ku, Tokyo, Ichiro Hasuo National Institute of Informatics, Japan | ||
11:30 30mPaper | 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 15mPaper | [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 | |||
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 |
14:00 - 15:30 | |||
14:00 30mPaper | Data Structures for Finite Downsets of Natural Vectors: Theory and Practice ATVA Papers | ||
14:30 30mPaper | 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 30mPaper | Antarbhukti: Verifying Correctness of PLC Software during System Evolution ATVA Papers |
14:00 - 15:30 | |||
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 Kentaro Kobayashi Department of Computer Science, University of Tsukuba, Yukiyoshi Kameyama University of Tsukuba | ||
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 |
16:00 - 17:30 | |||
16:00 30mPaper | Control Closure Certificates ATVA Papers | ||
16:30 30mPaper | Deriving Liveness Properties of Hybrid Systems from Reachable Sets and Lyapunov-like Certificates ATVA Papers | ||
17:00 15mPaper | [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 | |||
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 | |||
09:30 60mTalk | Network Abstractions for Modularity and Performance Verification Invited Talks Aarti Gupta Princeton University |
11:00 - 12:30 | |||
11:00 30mPaper | Energy Games with Weight Uncertainty ATVA Papers Orna Kupferman Hebrew University | ||
11:30 30mPaper | 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 30mPaper | 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 | |||
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 |
14:00 - 15:30 | 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 | ||
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, Thierry Jéron INRIA, Sayan Mukherjee Univ Rennes, Inria, CNRS, IRISA, France, Srinivas Pinisetty Indian Institute of Technology Bhubaneswar |
14:00 - 15:00 | |||
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 | |||
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 |
11:00 - 12:30 | |||
11:00 30mPaper | Inductive Generalization in Reinforcement Learning from Specifications ATVA Papers | ||
11:30 30mPaper | Locally Pareto-Optimal Interpretations for Black-Box Machine Learning Models ATVA Papers | ||
12:00 30mPaper | Solution-aware vs global ReLU selection: partial MILP strikes back for DNN verification ATVA Papers |
11:00 - 12:30 | |||
14:00 - 15:00 | |||
14:00 30mPaper | Towards Unified Probabilistic Verification and Validation of Vision based Autonomy ATVA Papers | ||
14:30 15mPaper | [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 15mPaper | [TOOL] Q-Sylvan: A Parallel Decision Diagram Package for Quantum Computing ATVA Papers |
14:00 - 15:00 | |||
15:00 - 16:00 | |||
15:00 60mTutorial | Quantitative and Probabilistic Verification Tutorials and Workshops Benjamin Lucien Kaminski Saarland University; University College London |
16:30 - 17:30 | |||
16:30 60mTutorial | Quantitative and Probabilistic Verification Tutorials and Workshops Benjamin Lucien Kaminski Saarland University; University College London |
Fri 31 OctDisplayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
Fri 31 Oct
Displayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
09:30 - 10:25 | |||
09:30 55mTalk | Talk 1 Tutorials and Workshops Ahmed Bouajjani IRIF, Université Paris Diderot |
11:00 - 12:55 | |||
11:00 55mTalk | Talk 2: Causally Deterministic (factored) Markov Decision Processes. Tutorials and Workshops | ||
12:00 55mTalk | Talk 3 Tutorials and Workshops Pavithra Prabhakar Kansas State University |
14:30 - 15:25 | |||
14:30 55mTalk | Talk 4: On the average-case complexity of the word problem in subgroups of GL_d(Z) Tutorials and Workshops |
16:00 - 17:00 | |||