CAV 2025
79 papers
- $\mathbf{{\textsc {PyCaliper}}}$: Python-Embedded Infrastructure for RTL Verification and Specification Synthesis
- A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
- A Formally Verified Robustness Certifier for Neural Networks
- A Misconception-Driven Adaptive Tutor for Linear Temporal Logic
- Accelerating Automated Program Verifiers by Automatic Proof Localization
- Accelerating Markov Chain Model Checking: Good-for-Games Meets Unambiguous Automata
- An Intermediate Program Representation for Optimizing Stream-Based Languages
- Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
- Approximating Fixpoints of Approximated Functions
- Arithmetizing Shape Analysis
- Assessing the Quality of Binomial Samplers: A Statistical Distance Framework
- Automata Learning from Preference and Equivalence Queries
- Automated Parameterized Verification of a Railway Protection System with Dafny
- Automated Verification of Consistency in Zero-Knowledge Proof Circuits
- Automated Verification of Monotonic Data Structure Traversals in C
- Automatic Synthesis of Smooth Infinite Horizon Paths Satisfying Linear Temporal Logic Specifications
- Automatic Verification of Floating-Point Accumulation Networks
- Branching Bisimulation Learning
- Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking
- Charon: An Analysis Framework for Rust
- Compositional Abstraction for Timed Systems with Broadcast Synchronization
- Counter Example Guided Reactive Synthesis for LTL Modulo Theories*
- Counterexample-Guided Commutativity
- Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks
- D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation
- Data-Driven Verification of Procedural Programs with Integer Arrays
- Decision Heuristics in MCSat
- Deductive Synthesis of Reinforcement Learning Agents for Infinite Horizon Tasks
- Deeply Optimizing the SAT Solver for the IC3 Algorithm
- Efficient Probabilistic Model Checking for Relational Reachability
- Engineering an Efficient Probabilistic Exact Model Counter
- Extending AALpy with Passive Learning: A Generalized State-Merging Approach
- FeynmanDD: Quantum Circuit Analysis with Classical Decision Diagrams
- Fifteen Years of Viper
- Floating-Point Neural Networks are Provably Robust Universal Approximators
- Full LTL Synthesis over Infinite-State Arenas
- INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition
- Infinite-State Liveness Checking with rlive
- Integer Reasoning Modulo Different Constants in SMT
- Introducing Certificates to the Hardware Model Checking Competition
- Issy: A Comprehensive Tool for Specification and Synthesis of Infinite-State Reactive Systems
- Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers
- LearnLib: 10 years later
- ModelVerification.jl: A Comprehensive Toolbox for Formally Verifying Deep Neural Networks
- NeuralSAT: A High-Performance Verification Tool for Deep Neural Networks
- On the Almost-Sure Termination of Probabilistic Counter Programs
- On the Complexity of Checking Mixed Isolation Levels for SQL Transactions
- POPACheck: A Model Checker for Probabilistic Pushdown Automata
- Panini: An Efficient and Flexible Knowledge Compiler
- Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates
- Polyregular Model Checking
- Property Directed Reachability with Extended Resolution
- PyEuclid: A Versatile Formal Plane Geometry System in Python
- QSM-Cutoff: Systematic Derivation of Quantified Cutoff Formulas for Distributed Protocols
- Quantitative Supermartingale Certificates
- Raven: An SMT-Based Concurrency Verifier
- Regex Decision Procedures in Extended RE#
- Relational Hoare Logic for Realistically Modelled Machine Code
- Robust Probabilistic Bisimilarity for Labelled Markov Chains
- Scaling GR(1) Synthesis via a Compositional Frameworkfor LTL Discrete Event Control
- Scaling Up Proactive Enforcement
- Small Decision Trees for MDPs with Deductive Synthesis
- Space Explanations of Neural Network Classification
- Sprout: A Verifier for Symbolic Multiparty Protocols
- StarV: A Qualitative and Quantitative Verification Tool for Learning-Enabled Systems
- StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs
- Structural Operational Semantics for Functional and Security Verification of Pipelined Processors
- Supermartingale Certificates for Quantitative Omega-Regular Verification and Control
- Surfer - An Extensible Waveform Viewer
- The Vampire Diary
- The rIC3 Hardware Model Checker
- Veil: A Framework for Automated and Interactive Verification of Transition Systems
- Verified and Optimized Implementation of Orthologic Proof Search
- Verifying Fault-Tolerance of Quantum Error Correction Codes
- Verifying PETSc Vector Components Using CIVL
- Verifying Tree-Manipulating Programs via CHCs
- lean-smt: An SMT Tactic for Discharging Proof Goals in Lean
- sfGPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency
- sfHornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses