CAV — PROGRAM
Days: Sunday, 26 July 2026 Monday, 27 July 2026 Tuesday, 28 July 2026 Wednesday, 29 July 2026
Sunday, 26 July 2026
10:00-10:30
Coffee Break
CAV
Location:
Grande Auditório
10:30-12:35
Verification of Parallel, Concurrent, and Distributed Systems
CAV
Session Chair:
Location:
Grande Auditório
| 10:30-10:45 |
On the Complexity of Checking Soundness of Natural Reductions (abstract) 15 min
1 LIX - CNRS - Ecole Polytechnique
2 University of Toronto
|
| 10:45-11:00 |
Deadlock Verification via Ordering-Constrained Mutex Modeling (abstract) 15 min
1 Tsinghua University
|
| 11:00-11:15 |
Complete Local Reasoning About Parameterized Programs Over Topologies (Distinguished Paper) (abstract) 15 min
1 University of Toronto
|
| 11:15-11:30 |
Scalable Deductive Verification of Data-Level Parallel Programs (abstract) 15 min
1 Eindhoven University of Technology
2 University of Twente
|
| 11:30-11:45 |
On the Verification Problem of Remote Direct Memory Access programs (abstract) 15 min
1 Uppsala University
2 The Institute of Mathematical Sciences, Chennai
|
| 11:45-11:55 |
Model Checking for Flexible Network Protocols (abstract) 10 min
1 Princeton University
2 Google, Inc
|
| 11:55-12:05 |
The TLA+ Model Checker Apalache (abstract) 10 min
1 University of Groningen
2 Tarides
3 Independent Researcher
4 Informal Systems
5 Université Paris-Saclay, CEA, List
|
| 12:05-12:15 |
PSF: A Generic and Extensible Framework for Protocol State Fuzzing (abstract) 10 min
1 Uppsala University & National Technical University of Athens
2 Yale University & National Technical University of Athens
|
| 12:15-12:25 |
Kofola 1.0: A Modular Approach to 𝝎-Regular Complementation and Inclusion Checking (abstract) 10 min
1 Brno University of Technology
2 Brno University of Technology and Aalborg University
3 Institute of Software, Chinese Academy of Sciences
4 Slovak University of Technology in Bratislava
|
| 12:25-12:35 |
Octopus: Practical Equivalence Checking of P4 Packet Parsers (abstract) 10 min
1 LIACS, Leiden University
|
12:30-14:00
Lunch
CAV
Location:
Grande Auditório
14:00-15:30
Synthesis
CAV
Session Chair:
Location:
Grande Auditório
| 14:00-14:15 |
Randomise Alone, Reach Together (abstract) 15 min
1 Institute of Science and Technology Austria
|
| 14:15-14:30 |
Decoupled Planning for Multiple Omega-Regular Objectives (abstract) 15 min
1 University of Haifa, Israel
2 Institute of Science and Technology, Austria
3 IMDEA Software Institute, Spain
4 TU Clausthal, Germany
|
| 14:30-14:45 |
Repairing Regex-Dependent String-Manipulation Programs (abstract) 15 min
1 NTT Social Informatics Laboratories
2 Waseda University
|
| 14:45-15:00 |
Liquid Tree Automata (abstract) 15 min
1 Indian Institute of Technology Hyderabad
2 Purdue University
|
| 15:00-15:10 |
SemML 2.0: Synthesizing Controllers from LTL (abstract) 10 min
1 TU Munich
2 Lancaster University Leipzig
3 Masaryk University Brno
|
| 15:10-15:20 |
Fast Obligation Translation and Synthesis (Distinguished Paper) (abstract) 10 min
1 LRE
2 University of Oxford
3 DIMAP, University of Warwick
4 University of Gothenburg & Chalmers University of Technology
5 Rice University
6 University of Liverpool
7 EPITA
|
| 15:20-15:30 |
sweap: Reactive Synthesis for Infinite-State Integer Problems (abstract) 10 min
1 Dedaub
2 TU Wien
3 University of Gothenburg, Chalmers University of Technology
|
15:30-16:00
Coffee Break
CAV
Location:
Grande Auditório
16:00-17:00
Hardware Verification
CAV
Session Chair:
Location:
Grande Auditório
| 16:00-16:15 |
A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking (abstract) 15 min
1 Hong Kong University of Science and Technology
2 Hong Kong University of Science and Technology (Guangzhou)
|
| 16:15-16:30 |
A Multi-Width Parametric Equivalence Solver (abstract) 15 min
1 University College London
2 Imperial College London
|
| 16:30-16:45 |
Massively Parallel Mining of Specifications for Hardware Designs (abstract) 15 min
1 University of Edinburgh
|
| 16:45-17:00 |
A mechanised, bidirectional type system for bit-width determination in SystemVerilog (abstract) 15 min
1 École normale supérieure – PSL
2 Imperial College London
|
Monday, 27 July 2026
09:00-10:00
Invited Talk
CAV
Session Chair:
Location:
Grande Auditório
| 09:00-10:00 |
Deriving Test Oracles for Verification Infrastructure (abstract) 60 min
1 TU Wien, Austria
|
10:00-10:30
Coffee Break
CAV
Location:
Grande Auditório
10:30-11:20
Security, Privacy and Hyperproperties
CAV
Session Chair:
Location:
Grande Auditório
| 10:30-10:45 |
Differentially Private Runtime Monitoring (abstract) 15 min
1 CISPA Helmholtz Center for Information Security
|
| 10:45-11:00 |
HyperLasso: Bounded Model Checking of ∀+∃+-Liveness Hyperproperties (abstract) 15 min
1 Universidade do Minho & INESC TEC
|
| 11:00-11:10 |
The Simulator’s Blueprint: Automata Learning from Cybersecurity Logs (abstract) 10 min
1 Cornell
2 EPFL
3 Tehran Institute for Advanced Studies, Khatam University
|
| 11:10-11:20 |
HyperQB 2.0: A Bounded Model Checker for Hyperproperties (abstract) 10 min
1 Michigan State University
|
11:20-12:30
SMT, SAT & Decision Procedures
CAV
Session Chair:
Location:
Grande Auditório
| 11:20-11:35 |
Improving Stability of SMT Solvers via Context-Driven Normalization (abstract) 15 min
1 Institute of Software, Chinese Academy of Sciences
2 Beihang University
|
| 11:35-11:50 |
Satisfiability Modulo Extensional Constant Arrays (Distinguished Paper) (abstract) 15 min
1 Stanford University
|
| 11:50-12:05 |
String Solving with Stabilization and Transducers (abstract) 15 min
1 Brno University of Technology
2 Aalborg University
|
| 12:05-12:20 |
Lagrangian-Based Duality for Quantified SMT Algorithms (abstract) 15 min
1 TU Wien
2 Chiba University
3 Tohoku University
4 Weizmann Institute of Science
5 Tel Aviv University
|
| 12:20-12:30 |
Mallob: Scalable Automated Reasoning On Demand (Distinguished Paper) (abstract) 10 min
1 Karlsruhe Institute of Technology
|
12:30-14:00
Lunch
CAV
Location:
Grande Auditório
14:00-15:30
Deductive Verification & Certified Verification
CAV
Session Chair:
Location:
Grande Auditório
| 14:00-14:15 |
Modular Reasoning about Object Relations (Distinguished Paper) (abstract) 15 min
1 ETH Zurich
|
| 14:15-14:30 |
Formally Verified Linear-Time Invertible Lexing (abstract) 15 min
1 EPFL
|
| 14:30-14:45 |
Automating Bitvector and Finite Field Equivalence Proofs in Lean (abstract) 15 min
1 Stanford University
2 Galois, Inc.
|
| 14:45-15:00 |
The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver (abstract) 15 min
1 The University of Iowa
2 Universidade Federal de Minas Gerais
3 Bar Ilan University
4 Stanford University
5 Amazon Web Services
|
| 15:00-15:10 |
Burrow: A Proof Framework for Weak Memory (abstract) 10 min
1 TU Munich
2 TU Delft
|
| 15:10-15:20 |
Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean (Distinguished Paper) (abstract) 10 min
1 National University of Singapore
2 Neapolis University Pafos
|
| 15:20-15:30 |
Automatic Heap-Memory Diagrams for Separation-Logic Proofs (abstract) 10 min
1 EPFL
|
15:30-16:00
Coffee Break
CAV
Location:
Grande Auditório
16:00-17:50
Automata
CAV
Session Chair:
Location:
Grande Auditório
| 16:00-16:15 |
An L# Based Algorithm for Active Learning of Minimal Separating Automata (abstract) 15 min
1 Radboud University
|
| 16:15-16:30 |
Upper Bound for the Determinization of Emerson-Lei Automata: A One-Fin Approach (abstract) 15 min
1 ICTT and ISN Laboratory, Xidian University
|
| 16:30-16:45 |
SMT-Based Active Learning of Weighted Automata (abstract) 15 min
1 University College London
2 Cornell University
|
| 16:45-17:00 |
Compositional Verification of Timed Automata via Violation Assumptions (abstract) 15 min
1 TU Wien, Austria - Sharif University of Technology, Iran
2 Sharif University of Technology, Iran
3 University of Tehran, Iran
4 Malardalen University, Sweden
|
| 17:00-17:15 |
Weighted soundness for Workflow Nets (abstract) 15 min
1 University of Warsaw
|
| 17:15-17:30 |
Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning (abstract) 15 min
1 Nanyang Technological University
2 Tata Institute of Fundamental Research
3 Université Libre de Bruxelles
4 Univ Rennes, Inria, CNRS, IRISA
|
| 17:30-17:40 |
TACO: A Toolsuite for the Verification of Threshold Automata (abstract) 10 min
1 CISPA Helmholtz Center for Information Security
2 American University of Beirut
3 Luxembourg University
|
| 17:40-17:50 |
Extending QuAK with Nested Quantitative Automata (abstract) 10 min
1 Institute of Science and Technology Austria (ISTA)
2 Slovak University of Technology in Bratislava
3 CISPA Helmholtz Center for Information Security
4 Sabancı University
|
18:00-19:00
Logic Lounge
CAV
Session Chair:
Location:
Grande Auditório
| 18:00-19:00 |
Proof Against Attack: Can AI Help Build Software We Can Trust? (abstract) 60 min
1 Advanced Research and Invention Agency
|
Tuesday, 28 July 2026
10:00-10:30
Coffee Break
CAV
Location:
Grande Auditório
10:30-12:25
Machine Learning, AI and Verification
CAV
Session Chair:
Location:
Grande Auditório
| 10:30-10:45 |
VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification (abstract) 15 min
1 University of Western Australia
2 University of Genova
|
| 10:45-11:00 |
QAV-FT: Quadratic Approximation-based Neural Network Verification via Fourier Series and Taylor Truncation (abstract) 15 min
1 School of Computer Science and Engineering, University of Electronic Science and Technology of China
2 College of Computer Science and Artificial Intelligence, Southwest Minzu University
|
| 11:00-11:15 |
The Rocq-NN-Roll Prover: Soundly Verifying Hyperproperties of Neural Networks in Rocq (abstract) 15 min
1 Fraunhofer Institute FOKUS Berlin
2 Technische Universität Berlin
|
| 11:15-11:30 |
ATKVerifier: Adaptive Top-K Constraints for Tighter Verification of Semantic Segmentation Networks (abstract) 15 min
1 ICTT and ISN Laboratory, Xidian University
2 KylinSoft Co., Ltd.
|
| 11:30-11:45 |
Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement (abstract) 15 min
1 Kyushu University
|
| 11:45-12:00 |
Quantifying Sensitivity for Tree Ensembles : A symbolic and compositional approach (abstract) 15 min
1 IIT Bombay
2 University of Toronto
|
| 12:00-12:15 |
Shields to Guarantee Probabilistic Safety in MDPs (abstract) 15 min
1 Radboud University
2 Brno University of Technology
|
| 12:15-12:25 |
A Neurosymbolic Approach to Natural Language Formalization and Verification (abstract) 10 min
1 Amazon Web Services
2 Amazon Web Services, University College London
3 University of Toronto
|
12:25-13:45
Lunch
CAV
Location:
Grande Auditório
13:45-14:45
CAV Award
CAV
Session Chair:
Location:
Grande Auditório
| 13:45-14:45 |
Invited talk by CAV Award awardees (abstract) 60 min
1 na
|
14:50-15:30
Liveness/Termination
CAV
Session Chair:
Location:
Grande Auditório
| 14:50-15:05 |
Liveness Proofs for Hardware Model Checking (Distinguished Paper) (abstract) 15 min
1 KU Leuven
2 Leiden University
3 University of Freiburg
4 University of Helsinki
|
| 15:05-15:20 |
Transition Invariants Revisited: Termination Witnesses and Their Validation (abstract) 15 min
1 LMU Munich
|
| 15:20-15:30 |
KoAT: Automatic Complexity and Termination Analysis of Integer Programs (abstract) 10 min
1 RWTH Aachen University
|
15:30-16:00
Coffee Break
CAV
Location:
Grande Auditório
16:00-17:25
Program Analysis Session
CAV
Session Chair:
Location:
Grande Auditório
| 16:00-16:15 |
Sound and Precise Symbolic Automata Model for Stateful Software Systems (abstract) 15 min
1 Nanjing University
2 Zhejiang University
|
| 16:15-16:30 |
Automated Amortised Analysis of Skew Heaps and Leftist Heaps (abstract) 15 min
1 University of Innsbruck
2 TU Eindhoven, Netherlands
3 Vienna University of Technology
|
| 16:30-16:45 |
Polynomial Invariant Generation for Floating-Point Programs (abstract) 15 min
1 University of Oxford
2 National University of Defense Technology
3 Shanghai University of Finance and Economics
|
| 16:45-17:00 |
Parallel Abstract Interpretation for Polynomial Programs with Range Bound Assertions (abstract) 15 min
1 Indian Institute of Technology Bombay
2 IIT Bombay
3 HKUST
4 University of Oxford
5 TU Wien
6 Singapore Management University
|
| 17:00-17:15 |
Incremental Inference for Probabilistic Datalog (abstract) 15 min
1 Purdue University
2 UT Austin
|
| 17:15-17:25 |
Automatic Detection of Reference Counting Bugs in Linux Kernel Drivers (Distinguished Paper) (abstract) 10 min
1 The University of Tokyo
|
17:30-18:00
CAV Business meeting
CAV
Location:
Grande Auditório
Wednesday, 29 July 2026
09:00-10:00
Invited Talk
CAV
Session Chair:
Location:
Grande Auditório
| 09:00-10:00 |
Formally Explaining Neural Networks (abstract) 60 min
1 Hebrew University of Jerusalem
|
10:00-10:30
Coffee Break
CAV
Location:
Grande Auditório
10:30-11:15
Software: Tools, Verification and Synthesis
CAV
Session Chair:
Location:
Grande Auditório
| 10:30-10:45 |
Consistency-Based Software Diagnosis: Accuracy, Scalability, and Limitations (abstract) 15 min
1 TU Wien
2 Monash University
|
| 10:45-10:55 |
Show Me The Money: An Exercise in Proof-Driven Software Understanding (abstract) 10 min
1 University of Waterloo
2 SRI
3 Entalus
4 Stellar Development Foundation
|
| 10:55-11:05 |
SvLibChecker: A Light-Weight Tool for Software Model Checking (abstract) 10 min
1 LMU Munich
|
| 11:05-11:15 |
PyCHC: a Framework for Certified Horn Solving and CHC-based Design (abstract) 10 min
1 University of Lugano
2 Argot Collective
3 University of Groningen
|
11:15-12:35
Quantum
CAV
Session Chair:
Location:
Grande Auditório
| 11:15-11:30 |
How Many Circuit Identities Are Needed to Generate All Others? (abstract) 15 min
1 Purdue University
2 Stony Brook University
|
| 11:30-11:45 |
A Practical Specification Language for Automatic Quantum Program Verification (abstract) 15 min
1 National Taiwan University
2 Academia Sinica
3 Brno University of Technology
|
| 11:45-12:00 |
Formal Verification of Quantum Ancilla Safety (abstract) 15 min
1 Key Laboratory of System Software (Chinese Academy of Sciences), Institute of Software Chinese Academy of Sciences, University of Chinese Academy of Sciences
2 Leiden University
3 University of Edinburgh
4 Key Laboratory of System Software (Chinese Academy of Sciences), Institute of Software Chinese Academy of Sciences
|
| 12:00-12:15 |
Model Checking Matrix Product States Against Linear Chain Logic (abstract) 15 min
1 East China Normal University
2 Chinese Academy of Sciences
|
| 12:15-12:25 |
Analysis and Verification of Quantum Communication Protocols in UPPAAL (abstract) 10 min
1 Aalborg University
|
| 12:25-12:35 |
Quokka#: Quantum Computing with #SAT (abstract) 10 min
1 Leiden University
2 Delft University of Technology, Leiden University
3 Delft University of Technology
|
12:35-14:00
Lunch
CAV
Location:
Grande Auditório
14:00-16:00
Hybrids, Controls and Probabilistic Systems
CAV
Session Chair:
Location:
Grande Auditório
| 14:00-14:15 |
Over-approximation of weakly-hard constraints for control systems verification (abstract) 15 min
1 Saarland University
|
| 14:15-14:30 |
Spatiotemporal Robustness of Temporal Logic Tasks using Multi-Objective Reasoning (abstract) 15 min
1 ETH Zürich
|
| 14:30-14:45 |
Best-Effort Safety Control of Multi-Mode Systems (abstract) 15 min
1 University of Naples, Italy
|
| 14:45-15:00 |
Perception with Guarantees: Certified Pose Estimation via Reachability Analysis (abstract) 15 min
1 Technical University of Munich
2 University of California, Irvine
|
| 15:00-15:15 |
Tensor Probabilistic Model Checking of Finite-Horizon Markov Chains (abstract) 15 min
1 University of Waterloo
|
| 15:15-15:30 |
Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families (abstract) 15 min
1 Brno University of Technology
2 Radboud University
3 RWTH Aachen University
|
| 15:30-15:40 |
Ensuring Safety in Automotive Machine Learning Inference: From Pre-validated Static Kernels to Machine Learning Graph Compilation (abstract) 10 min
1 NVIDIA
|
| 15:40-15:50 |
Caesar: A Deductive Verifier for Probabilistic Programs (abstract) 10 min
1 RWTH Aachen University
2 Cornell University
3 Saarland University and University College London
4 DTU Compute and University of Oldenburg
|
| 15:50-16:00 |
ULTIMATE: A Tool for the Verification and Synthesis of Stochastic World Models (abstract) 10 min
1 University of York
|
16:00-16:30
Coffee Break
CAV
Location:
Grande Auditório