APLAS & ATVA 2026 (series) /
APLAS & ATVA 2026 Program
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
This program is tentative and subject to change.
Tue 1 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
Tue 1 Dec
Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
09:30 - 10:30 | APLAS NIER - Session 1NIER | ||
09:30 - 10:30 | ATVA Spotlights of Verification - Session 1ATVA Research Papers | ||
11:00 - 12:30 | APLAS NIER - Session 2NIER | ||
11:00 - 12:30 | ATVA Spotlights of Verification - Session 2ATVA Research Papers | ||
11:00 15mTalk | Verifying repeat-until-success protocols using automata ATVA Research Papers Yu-Fang Chen Academia Sinica, Jyun-Ao Lin National Taipei University of Technology, Jakub Havlík Brno University of Technology, Ondřej Lengál Brno University of Technology, Fang-Yi Lo Academia Sinica, Wei-Lun Tsai Academia Sinica, You-Jie Wu National Taipei University of Technology | ||
11:18 15mTalk | String Diagrams for Probabilistic Computation: From Completeness to Verification ATVA Research Papers Robin Piedeleu University of Oxford, Mateo Torres-Ruiz University College London, Alexandra Silva Cornell University, Fabio Zanasi University College London | ||
11:36 15mTalk | Verifying Quantum Programs: Quantum Markov Chains and Beyond ATVA Research Papers Ji Guan Institute of Software, Chinese Academy of Sciences | ||
11:54 15mTalk | SuperDP: Differential Privacy Refutation via Supermartingales ATVA Research Papers Krishnendu Chatterjee IST Austria, Ehsan Kafshdar Goharshady IST Austria, Đorđe Žikelić Nanyang Technological University | ||
12:12 15mTalk | Model Checking Matrix Product States Against Linear Chain Logic ATVA Research Papers Ming Xu East China Normal University, Yihao Chen East China Normal University, China, Ji Guan Institute of Software, Chinese Academy of Sciences | ||
14:00 - 15:30 | APLAS NIER - Session 3NIER | ||
14:00 - 15:30 | ATVA Spotlights of Verification - Session 3ATVA Research Papers | ||
14:00 15mTalk | Verifying the Rust Standard Library ATVA Research Papers Felipe R. Monteiro Amazon | ||
14:18 15mTalk | Data-Aware and Scalable Sensitivity Analysis for Decision Tree Ensembles ATVA Research Papers Namrita Varshney IIT Bombay, Ashutosh Gupta , Arhaan Ahmad IIT Bombay, Tanay V. Tayal IIT Bombay, S. Akshay Indian Institute of Technology, Bombay, India | ||
14:36 15mTalk | Verification of Competition-Level Algorithmic Programs with LLM ATVA Research Papers Lixiang Wang Shanghai Jiao Tong University, Xiwei Wu Shanghai Jiao Tong University, Zitong Ni Shanghai Jiao Tong University, Lihan Xie Shanghai Jiao Tong University, Shushu Wu Shanghai Jiao Tong University, Qinxiang Cao Shanghai Jiao Tong University | ||
14:54 15mTalk | Complementing Emerson-Lei Elevator Automata ATVA Research Papers Ondrej Alexaj Brno University of Technology, Vojtěch Havlena Brno University of Technology, Ondřej Lengál Brno University of Technology, Yong Li Institute of Software, Chinese Academy of Sciences, Nicolas Mazzocchi Slovak University of Technology in Bratislava | ||
15:12 15mTalk | Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features ATVA Research Papers Anne M. Tumlin Vanderbilt University, Ben Wooding Vanderbilt University, Zhenxuan Shao Vanderbilt University, Diego Manzanas Lopez Vanderbilt University, Tyler Derr Vanderbilt University, Taylor T Johnson Vanderbilt University | ||
16:00 - 17:30 | APLAS NIER - Session 4NIER | ||
16:00 - 17:30 | ATVA Spotlights of Verification - Session 4ATVA Research Papers | ||
Wed 2 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
Wed 2 Dec
Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
09:30 - 10:30 | Joint APLAS/ATVA KeynoteAPLAS Research Papers / ATVA Research Papers / Keynotes | ||
09:30 60mKeynote | Relational Program Logics for Probabilistic and Quantum Computations Keynotes Gilles Barthe MPI-SP; IMDEA Software Institute | ||
11:00 - 12:30 | Formal languages, program transformation, compilationAPLAS Research Papers | ||
11:00 30mTalk | Derivatives of Regular Expressions with Lookarounds APLAS Research Papers | ||
11:30 30mTalk | Reconciling Efficiency and Modularity in Metaprogramming via Shortcut Fusion APLAS Research Papers | ||
12:00 30mTalk | Tensors by Implementation, Records by Nature: Compiler Support for Neural Network Abstractions APLAS Research Papers Lauren Pudney The University of Western Australia, Gusts Gustavs Grīnbergs IT University of Copenhagen, Matthew L. Daggitt University of Western Australia | ||
11:00 - 12:30 | AutomataATVA Research Papers | ||
11:00 30mTalk | Prove: A Runtime Monitor of Linear Temporal Properties over Partial Order Executions ATVA Research Papers Moran Omer Bar Ilan University, Israel, Doron Peled Bar Ilan University, Borzoo Bonakdarpour Michigan State University, Anik Momtaz Michigan State University | ||
11:30 30mTalk | The Emptiness Problem for Quantum Finite Automata with Classical States ATVA Research Papers Di-De Yen Academia Sinica, Patrick Totzke University of Liverpool, Yun Chen Tsai National Institute of Informatics, Japan, Jyun-Ao Lin National Taipei University of Technology | ||
12:00 30mTalk | Universality of 1-Variable Automata is Decidable ATVA Research Papers Franziska Alber University of Regensburg, Philipp Rümmer University of Regensburg and Uppsala University | ||
14:00 - 15:30 | FoundationsAPLAS Research Papers | ||
14:00 30mTalk | Axiomatization of Ready Trace Equivalence for Regular Processes APLAS Research Papers Shining Zang Institute of Logic and Cognition, Sun Yat-sen University | ||
14:30 30mTalk | Dinaturals Compose, Up-to Loops APLAS Research Papers Andrea Laretto Tallinn University of Technology, Fosco Loregian Tallinn University of Technology, Niccolò Veltri Tallinn University of Technology | ||
15:00 30mTalk | Statically Typed Purely Functional Definitional Interpreters for Essentials of Programming Languages APLAS Research Papers Kwanghoon Choi Chonnam National University | ||
14:00 - 15:30 | |||
16:00 - 17:30 | |||
16:00 30mTalk | Fuzzy type theory APLAS Research Papers Shreya Arya UPenn, Greta Coraglia MIRAI, Paige Randall North Utrecht University, Juli O’Connor Carnegie Mellon University, Ana Luiza Tenorio Getulio Vargas Foundation, Hans Riess Georgia Institute of Technology | ||
16:30 30mTalk | Static Recognition of Fast-Paths for Effect Handlers APLAS Research Papers | ||
17:00 30mTalk | Unifying Function- and Argument-First Bidirectional Type Systems APLAS Research Papers Takuma Yoshioka Kyoto University, Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University | ||
16:00 - 17:30 | Games and synthesisATVA Research Papers | ||
16:00 30mTalk | From Fixed to Reconfigurable Communication: Bisimulation-Based Distributed Realization ATVA Research Papers Yehia Abd Alrahman The University of Gothenburg and Chalmers University of Technology, Nir Piterman University of Gothenburg and Chalmers University of Technology | ||
16:30 30mTalk | Towards Actionable Strategy Certificates in Stochastic Parity Games ATVA Research Papers Christel Baier TU Dresden, Germany, Diane Cauquil TU Dresden / ENS Paris-Saclay, Calvin Chau TU Dresden, Sascha Klüppelholz TU Dresden, Anne-Kathrin Schmuck Max Planck Institute for Software Systems | ||
Thu 3 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
Thu 3 Dec
Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
09:30 - 10:30 | APLAS KeynoteAPLAS Research Papers / ATVA Research Papers / Keynotes | ||
09:30 60mKeynote | Lean as a Multi-Modal Meta-Verifier Keynotes Ilya Sergey National University of Singapore | ||
11:00 - 12:30 | SemanticsAPLAS Research Papers | ||
11:00 30mTalk | Isoqueric: A Discipline and Monad for Safe-by-Construction, Query-Answer-Preserving Graph Extension APLAS Research Papers Casper Bach University of Southern Denmark | ||
11:30 30mTalk | Modular Relational Abstract Interpretation of WebAssembly APLAS Research Papers Saïd Zuhair OCamlPro; Université Paris-Saclay - CEA LIST, Léo Andrès , Matthieu Lemerre Université Paris-Saclay - CEA LIST | ||
12:00 30mTalk | Skeletal Semantics for WebAssembly: Structure and Interpretations APLAS Research Papers Sean Kristian Remond Harbo Aalborg University, Hans Hüttel Aalborg University, Thomas P. Jensen INRIA Rennes | ||
11:00 - 12:30 | Probabilistic systemsATVA Research Papers | ||
11:00 30mTalk | Extending PRCTL with conditional expected reward operators ATVA Research Papers Eshita Zaman Utah Valley University, Gianfranco Ciardo Iowa State University, Andrew S. Miner Iowa State University | ||
11:30 30mTalk | Ragtimer 1.0: Rapid Rare-Event Partial State Space Construction for Stochastic VAS ATVA Research Papers Landon Taylor Utah State University, Joshua Jeppson Utah State University, Bingqing Hu Utah State University, Lukas Buecherl Utah State University, Zhen Zhang Utah State University | ||
12:00 30mTalk | Supermartingale Certificates for Parametric MDPs ATVA Research Papers | ||
14:00 - 15:30 | VerificationAPLAS Research Papers | ||
14:00 30mTalk | Beyond Locksets and Thread IDs: Enhanced Static Data Race Detection APLAS Research Papers Daniel Bund Technical University of Munich, Julian Erhard CISPA, Michael Petter Technische Universität München, Michael Schwarz National University of Singapore | ||
14:30 30mTalk | Characterizing and Verifying Active Object Programs with Trace Logic APLAS Research Papers Niklas Heidler Technical University Darmstadt, Software Engineering Group, Reiner Hähnle Technical University of Darmstadt | ||
15:00 30mTalk | Extracting Functional Properties from Verified Imperative Programs APLAS Research Papers Zixun Guo Peking University, Yiyuan Cao Peking University, Di Wang Peking University, Zhenjiang Hu Peking University | ||
14:00 - 15:30 | |||
16:00 - 17:30 | APLAS Session 6APLAS Research Papers | ||
16:00 - 17:30 | Software IATVA Research Papers | ||
16:00 30mTalk | Synthesizing Probabilistic Saturating Counters with Differentially Private Formal Guarantees ATVA Research Papers Zhiming Chi Institute of Software, Chinese Academy of Sciences, Lutan Zhao Institute of Information Engineering, CAS, Depeng Liu Institute of Software, Chinese Academy of Sciences, Yong Li Institute of Software, Chinese Academy of Sciences, Pengfei Yang Institute of Software at Chinese Academy of Sciences, China, Bow-Yaw Wang , Rui Hou Institute of Information Engineering, CAS, Cheng-Chao Huang Nanjing Institute of Software Technology, ISCAS, Andrea Turrini Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences, Naijun Zhan | ||
16:30 30mTalk | SyOpt: Constrained Genetic Algorithm for Near-Optimal Resilient Routing Synthesis ATVA Research Papers Csaba Györgyi University of Vienna, Kim Larsen Aalborg University, Stefan Schmid TU Berlin, Germany, Jiri Srba Aalborg University | ||
Fri 4 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
Fri 4 Dec
Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
09:30 - 10:30 | ATVA KeynoteAPLAS Research Papers / ATVA Research Papers / Keynotes | ||
11:00 - 12:30 | Software IIATVA Research Papers | ||
11:00 30mTalk | Bit-Precise CHC Satisfiability Using Theory-Modular Reasoning ATVA Research Papers Omer Rappoport Technion - Israel Institute of Technology, Orna Grumberg Technion – Israel Institute of Technology, Yakir Vizel Technion—Israel Institute of Technology | ||
11:30 30mTalk | How Often Does Your Program Fail?Distinguished Paper ATVA Research Papers | ||
12:00 30mTalk | Spectral - Translating Specifications for Deductive Verification into LLVM-IR ATVA Research Papers | ||
14:00 - 15:30 | Verifying ML modelsATVA Research Papers | ||
14:00 30mTalk | NNV3: Expanding Neural Network Verification to New Architectures and Domains ATVA Research Papers Anne M. Tumlin Vanderbilt University, Samuel Sasaki Vanderbilt University, Ben Wooding Vanderbilt University, Diego Manzanas Lopez Vanderbilt University, Muhammad Usama Zubair The University of Texas at Dallas, Navid Hashemi Vanderbilt University, Hongchao Zhang Vanderbilt University, Waseem Abbas The University of Texas at Dallas, Ipek Oguz Vanderbilt University, Meiyi Ma Vanderbilt University, Taylor T Johnson Vanderbilt University | ||
14:30 30mTalk | Verification of Dimension-Squeezed Neural Networks via Latent Quantization ATVA Research Papers Semaan Douglas Wehbe Stony Brook University, Andrew Mata Stony Brook University, Alireza Aghaei Stony Brook University, Stanley Bak Stony Brook University | ||
15:00 30mTalk | Verifying Glitches in Decision Tree EnsemblesDistinguished Paper ATVA Research Papers Satyankar Chandra IIT Bombay, Harsh Chaurasia IIT Bombay, Ashutosh Gupta Indian Institute of Technology Bombay, Kaushik Mallik IMDEA Software Institute, Shankaranarayanan Krishna IIT Bombay, Namrita Varshney IIT Bombay | ||
16:00 - 17:30 | ExplainabilityATVA Research Papers | ||
16:00 30mTalk | Neuron Activation-based Computation of Logical Explanations for Deep Neural Networks ATVA Research Papers Tomáš Kolárik University of Lugano, Faezeh Labbaf University of Lugano, Fabrizio Leopardi University of Lugano, Grigory Fedyukovich Florida State University, Michael Wand Dalle Molle Institute for Artificial Intelligence USI-SUPSI, Natasha Sharygina USI Lugano, Switzerland | ||
16:30 30mTalk | Sufficient Reasons and Explanations for Reactive Systems ATVA Research Papers | ||