CAV 2024
69 papers
- A Framework for Debugging Automated Program Verification Proofs via Proof Actions
- Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
- Approximate Relational Reasoning for Quantum Programs
- Arithmetic Solving in Z3
- Avoiding the Shoals - A New Approach to Liveness Checking
- Bisimulation Learning
- Boosting Few-Pixel Robustness Verification via Covering Verification Designs
- Breaking the Mold: Nonlinear Ranking Function Synthesis Without Templates
- CaDiCaL 2.0
- Certified Robust Accuracy of Neural Networks Are Bounded Due to Bayes Errors
- Collective Contracts for Message-Passing Parallel Programs
- Compositional Value Iteration with Pareto Caching
- Distributed SMT Solving Based on Dynamic Variable-Level Partitioning
- Dynamic Programming for Symbolic Boolean Realizability and Synthesis
- Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
- Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification
- End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT
- Formally Certified Approximate Model Counting
- From Clauses to Klauses
- General Anticipatory Runtime Verification
- Guiding Enumerative Program Synthesis with Large Language Models
- Hevm, a Fast Symbolic Execution Framework for EVM Bytecode
- Information Flow Guided Synthesis with Unbounded Communication
- Inner-Approximate Reachability Computation via Zonotopic Boundary Analysis
- Interactive Theorem Proving Modulo Fuzzing
- LTL Learning on GPUs
- Lexicographic Ranking Supermartingales with Lazy Lower Bounds
- Localized Attractor Computations for Infinite-State Games
- Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
- Measurement-Based Verification of Quantum Markov Chains
- Monitizer: Automating Design and Evaluation of Neural Network Monitors
- Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-Learned
- On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches
- Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications
- Parsimonious Optimal Dynamic Partial Order Reduction
- Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games
- Predictive Monitoring with Strong Trace Prefixes
- Proactive Real-Time First-Order Enforcement
- Probabilistic Access Policies with Automated Reasoning Support
- QReach: A Reachability Analysis Tool for Quantum Markov Chains
- Quantified Linear Arithmetic Satisfiability via Fine-Grained Strategy Improvement
- Regular Reinforcement Learning
- Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automata
- SMLP: Symbolic Machine Learning Prover
- SMT-Based Symbolic Model-Checking for Operator Precedence Languages
- Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models
- Scalable Bit-Blasting with Abstractions
- Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
- Simulating Quantum Circuits by Model Counting
- SolTG: A CHC-Based Solidity Test Case Generator
- Split Gröbner Bases for Satisfiability Modulo Finite Fields
- Stochastic Omega-Regular Verification and Control with Supermartingales
- Strided Difference Bound Matrices
- Syntax-Guided Automated Program Repair for Hyperproperties
- Synthesis of Temporal Causality
- Testing the Migration from Analog to Software-Based Railway Interlocking Systems
- The MoXI Model Exchange Tool Suite
- The SemGuS Toolkit
- The Top-Down Solver Verified: Building Confidence in Static Analyzers
- The VerCors Verifier: A Progress Report
- Toward Liveness Proofs at Scale
- Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
- Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems
- Verification Algorithms for Automated Separation Logic Verifiers
- Verifying Cake-Cutting, Faster
- Verifying Global Two-Safety Properties in Neural Networks with Confidence
- What Should Be Observed for Optimal Reward in POMDPs?
- mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic
- soid: A Tool for Legal Accountability for Automated Decision Making