CAV 2026
82 papers
- A - tt IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking
- A Mechanised, Bidirectional Type System for Bit-Width Determination in SystemVerilog
- A Multi-width Parametric Bitvector Equivalence Solver
- A Neurosymbolic Approach to Natural Language Formalization and Verification
- A Practical Specification Language for Automatic Quantum Program Verification
- ATKVerifier: Adaptive Top-K Constraints for Tighter Verification of Semantic Segmentation Networks
- An L# Based Algorithm for Active Learning of Minimal Separating Automata
- Analysis and Verification of Quantum Communication Protocols in UPPAAL
- Automated Amortised Analysis of Skew Heaps and Leftist Heaps
- Automatic Detection of Reference Counting Bugs in Linux Kernel Drivers
- Automatic Heap-Memory Diagrams for Separation-Logic Proofs
- Automating Bitvector and Finite Field Equivalence Proofs in Lean
- Best-Effort Safety Control of Multi-mode Systems
- Burrow: A Proof Framework for Weak Memory
- Caesar: A Deductive Verifier for Probabilistic Programs
- Complete Local Reasoning About Parameterized Programs Over Topologies
- Compositional Verification of Timed Automata via Violation Assumptions
- Consistency-Based Software Diagnosis: Accuracy, Scalability, and Limitations
- Deadlock Verification via Ordering-Constrained Mutex Modeling
- Decoupled Planning for Multiple Omega-Regular Objectives
- Differentially Private Runtime Monitoring
- Ensuring Safety in Automotive Machine Learning Inference: From Pre-validated Static Kernels to Machine Learning Graph Compilation
- Extending QuAK with Nested Quantitative Automata
- Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families
- Fast Obligation Translation and Synthesis
- Formal Verification of Quantum Ancilla Safety
- Formally Verified Linear-Time Invertible Lexing
- How Many Quantum Circuit Identities Are Needed to Generate All Others?
- HyperLasso: Bounded Model Checking of ∀+∃>+-Liveness Hyperproperties
- HyperQB 2.0: A Bounded Model Checker for Hyperproperties
- Improving Stability of SMT Solvers via Context-Driven Normalization
- Incremental Inference for Probabilistic Datalog
- KoAT: Automatic Complexity and Termination Analysis of Integer Programs
- Kofola 1.0: A Modular Approach to ømega-Regular Complementation and Inclusion Checking
- Lagrangian-Based Duality for Quantified SMT Algorithms
- Learning to Split: A Reinforcement-Learning-Guided Splitting Heuristic for Neural Network Verification (Invited Talk)
- Liquid Tree Automata
- Liveness Proofs for Hardware Model Checking
- Mallob: Scalable Automated Reasoning on Demand
- Massively Parallel Mining of Specifications for Hardware Designs
- Model Checking Matrix Product States Against Linear Chain Logic
- Model Checking for Flexible Network Protocols
- Modular Reasoning About Object Relations
- Octopus: Practical Equivalence Checking of P4 Packet Parsers
- On the Complexity of Checking Soundness of Natural Reductions
- On the Verification Problem of Remote Direct Memory Access Programs
- Over-Approximation of Weakly-Hard Constraints for Control Systems Verification
- PSF: A Generic and Extensible Framework for Protocol State Fuzzing
- Parallel Abstract Interpretation for Polynomial Programs with Range Bound Assertions
- Perception with Guarantees: Certified Pose Estimation via Reachability Analysis
- Polynomial Invariant Generation for Floating-Point Programs
- Precise Verification of Transformers Through ReLU-Catalyzed Abstraction Refinement
- PyCHC: A Framework for Certified Horn Solving and CHC-Based Design
- QAV-FT: Quadratic Approximation-Based Neural Network Verification via Fourier Series and Taylor Truncation
- Quantifying Sensitivity for Tree Ensembles: A Symbolic and Compositional Approach
- Quokka#: Quantum Computing with #SAT
- Randomise Alone, Reach as a Team
- Repairing Regex-Dependent String-Manipulation Programs
- SMT-Based Active Learning of Weighted Automata
- Satisfiability Modulo Extensional Constant Arrays
- Scalable Deductive Verification of Data-Level Parallel Programs
- SemML 2.0: Synthesizing Controllers for LTL
- Shields to Guarantee Probabilistic Safety in MDPs
- Show Me The Money: An Exercise in Proof-Driven Software Understanding
- Sound and Precise Symbolic Automata Model for Stateful Software Systems
- Spatiotemporal Robustness of Temporal Logic Tasks Using Multi-Objective Reasoning
- String Solving with Stabilization and Transducers
- SvLibChecker: A Light-Weight Tool for Software Model Checking
- Synthesizing POMDP Policies: Sampling Meets Model-Checking via Learning
- TACO: A Toolsuite for the Verification of Threshold Automata
- Tensor Probabilistic Model Checking of Finite-Horizon Markov Chains
- The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver
- The Rocq-NN-Roll Prover: Soundly Verifying Hyperproperties of Neural Networks in Rocq
- The Simulator's Blueprint: Automata Learning from Cybersecurity Logs
- The TLA+ Model Checker Apalache
- Transition Invariants Revisited: Termination Witnesses and Their Validation
- ULTIMATE: A Tool for the Verification and Synthesis of Stochastic World Models
- Upper Bound for the Determinization of Emerson-Lei Automata: A One-Fin Approach
- VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification
- Velvet: A Foundational Multi-modal Verifier for Imperative Programs in Lean
- Weighted Soundness for Workflow Nets
- sweap: Reactive Synthesis for Infinite-State Integer Problems