Computer Aided Verification : : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I.

• Superior document: Lecture Notes in Computer Science Series ; v.14681
• Author: Gurfinkel, Arie.
• TeilnehmendeR: Ganesh, Vijay.
• Place / Publishing House: Cham : : Springer International Publishing AG,, 2024.; ©2024.
• Year of Publication: 2024
• Edition: 1st ed.
• Language: English
• Series: Lecture Notes in Computer Science Series
• Physical Description: 1 online resource (523 pages)

Table of Contents

• Intro
• Preface
• Organization
• Invited Talks
• How to Solve Math Problems Without Talent
• Bridging Formal Mathematics and Software Verification
• The Art of SMT Solving
• Contents - Part I
• Contents - Part II
• Contents - Part III
• Decision Procedures
• Split Gröbner Bases for Satisfiability Modulo Finite Fields
• 1 Introduction
• 1.1 Related Work
• 2 Background
• 3 Motivating Example
• 3.1 Verifying the Determinism of Num2Bits
• 3.2 The Challenge of Bit-Splitting
• 3.3 Cooperative Reasoning: A Path Forward
• 4 Approach
• 4.1 Split Gröbner bases
• 4.2 Abstract Procedure: Split
• 4.3 Concrete Procedure: BitSplit
• 5 Experiments
• 5.1 Benchmarks
• 5.2 Comparison to Prior Solvers
• 5.3 Comparison to Variants
• 6 Application
• 6.1 Background on Verifiable Field-Blasting
• 6.2 A New Strategy for Verifying Operator Rules
• 7 Conclusion
• A Additional Background
• B Computing Bitsum Usage in Real World Projects
• C Proof of Theorem 1
• D Proof of Theorems 2 and 3
• E Proof of Lemma 1
• F The Seq Benchmark Family
• G Proof of Theorem 4
• References
• Arithmetic Solving in Z3
• 1 Introduction
• 2 Design Goals and Implementation Choices
• 3 Linear Real Arithmetic
• 3.1 Linear Solving
• 3.2 Finding Equal Variables - Cheaply
• 3.3 Bounds Propagation
• 4 Integer Linear Arithmetic
• 4.1 Patching
• 4.2 Cubes
• 4.3 GCD Consistency
• 4.4 Branching
• 4.5 Cuts
• 5 Non-linear Arithmetic
• 5.1 Patch Monomials
• 5.2 Bounds Propagation
• 5.3 Adding Bounds
• 5.4 Gröbner reduction
• 5.5 Incremental Linearization
• 5.6 NLSat
• 6 Shared Equalities
• 7 Evaluation
• 8 Summary and Discussion
• References
• Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
• 1 Introduction
• 2 Preliminaries
• 3 Classical Automata-Based Decision Procedure for LIA.
• 4 Derivative-Based Construction for Nested Formulae
• 5 Simple Rewriting Rules
• 6 Disjunction Pruning
• 7 Quantifier Instantiation
• 7.1 Quantifier Instantiation Based on Formula Monotonicity
• 7.2 Range-Based Quantifier Instantiation
• 7.3 Modulo Linearization
• 8 A Comprehensive Example of Our Optimizations
• 9 Experimental Evaluation
• 10 Related Work
• References
• Distributed SMT Solving Based on Dynamic Variable-Level Partitioning
• 1 Introduction
• 2 Preliminaries
• 2.1 Definitions and Notations
• 2.2 Parallel SMT Solving with Partitioning
• 2.3 Interval Constraint Propagation
• 3 Dynamic Parallel Framework Based on Arithmetic Partitioning
• 3.1 The Framework
• 3.2 Partition Tree Maintenance and UNSAT Propagation
• 3.3 Terminate on Demand
• 3.4 A Running Example
• 4 Variable-Level Partitioning for Arithmetic Theories
• 4.1 Preprocessing
• 4.2 The Partitioning Algorithm
• 4.3 BICP in Arithmetic Partitioning
• 5 Evaluation
• 5.1 Evaluation Preliminaries
• 5.2 Comparison to Sequential Solving
• 5.3 Comparison to State-of-the-art Partitioning Strategies
• 5.4 Improvement on Pure-Conjunction Formulas
• 6 Conclusion and Future Work
• References
• Quantified Linear Arithmetic Satisfiability via Fine-Grained Strategy Improvement
• 1 Introduction
• 2 Fine-Grained Game Semantics for LRA Satisfiability
• 2.1 Linear Rational Arithmetic
• 2.2 Fine-Grained Game Semantics
• 3 Fine-Grained Strategy Skeletons
• 4 Fine-Grained Strategy Improvement
• 5 Computing Counter-Strategies
• 5.1 Term Selection
• 6 Synthesizing Fine-Grained Strategies
• 7 Experimental Evaluation
• 8 Discussion and Related Works
• References
• From Clauses to Klauses*
• 1 Introduction
• 2 Background
• 2.1 Cardinality Constraints
• 2.2 Conflict-Driven Clause Learning and Proofs of Unsatisfiability.
• 3 At-Least-K Conjunctive Normal Form (KNF)
• 4 Cardinality Constraint Extraction and Analysis
• 4.1 Extraction
• 4.2 Analysis with BDDs
• 4.3 PySAT Encodings Experimental Evaluation
• 5 Cardinality Conflict-Driven Clause Learning
• 5.1 Implementation Details
• 5.2 Inprocessing Techniques
• 6 Proof Checking
• 6.1 Satisfying Assignments
• 6.2 Clausal Proofs
• 6.3 Starting with KNF Input
• 7 Experimental Evaluation
• 7.1 SAT Competition Benchmarks
• 7.2 Magic Squares and Max Squares
• 8 Conclusion and Future Work
• References
• CaDiCaL 2.0
• 1 Introduction
• 2 Architecture
• 3 External Propagator
• 4 Proofs
• 5 Tracer Interface
• 6 Constraints and Flipping
• 7 Interpolation
• 8 Testing and Debugging
• 9 Experiments
• 10 Conclusion
• References
• Formally Certified Approximate Model Counting
• 1 Introduction
• 2 Related Work
• 3 Background
• 3.1 Approximate Model Counting
• 3.2 Formalization in Isabelle/HOL
• 4 Approximate Model Counting in Isabelle/HOL
• 4.1 Abstract Specification and Probabilistic Analysis
• 4.2 Concretization to a Certificate Checker
• 4.3 Extending ApproxMC to ApproxMCCert
• 4.4 CNF-XOR Unsatisfiability Checking
• 5 Experimental Evaluation
• 6 Conclusion and Future Work
• References
• Scalable Bit-Blasting with Abstractions
• 1 Introduction
• 2 Preliminaries
• 3 Abstraction-Refinement Framework
• 4 Refinement Schemes
• 4.1 Hand-Crafted Lemmas
• 4.2 Lemma Scoring Scheme
• 4.3 Synthesizing Lemmas via Abduction
• 4.4 Lemma Verification
• 5 Integration
• 6 Evaluation
• 7 Conclusion
• References
• Hardware Model Checking
• The MoXI Model Exchange Tool Suite
• 1 Overview
• 2 Intermediate Language
• 3 Tool Suite
• 3.1 Translators
• 3.2 Utilities
• 4 Tool Suite Validation
• 5 Benchmarks
• 6 Conclusion and Future Work
• References
• SMLP: Symbolic Machine Learning Prover.
• 1 Introduction
• 2 SMLP Architecture
• 3 Symbolic Representation of Models and Constraints
• 4 Symbolic Representation of the ML Model Exploration
• 5 Problem Specification in SMLP
• 6 SMLP Exploration Modes of ML Models
• 6.1 Stable Parameter Synthesis
• 6.2 Verifying Assertions on a Model
• 6.3 Querying Conditions on the Model
• 6.4 Stable Optimized Synthesis
• 6.5 Design of Experiments
• 6.6 Root Cause Analysis
• 6.7 Model Refinement Loop
• 7 Implementation
• 8 Industrial Case Studies
• 9 Future Work
• References
• Avoiding the Shoals - A New Approach to Liveness Checking
• 1 Introduction
• 2 Preliminaries
• 2.1 Boolean Satisfiability
• 2.2 Boolean Transition Systems
• 2.3 Invariant Checking
• 2.4 Liveness Checking
• 3 Liveness Checking with rlive
• 3.1 Overview
• 3.2 Algorithm
• 3.3 Optimizations
• 3.4 Correctness Proof
• 4 Related Work
• 5 Evaluation
• 5.1 Experimental Setup
• 5.2 Experimental Results
• 6 Conclusions
• References
• Toward Liveness Proofs at Scale
• 1 Introduction
• 2 Background and Related Work
• 2.1 Liveness-to-Safety with Rankings
• 2.2 Dynamic Liveness-to-Safety Construction
• 3 Relational Rankings
• 3.1 The Relational Reactivity Rule
• 3.2 Chaining Liveness Lemmas
• 3.3 Stable Schedulers
• 3.4 Lexicographic Rankings
• 4 Case Study: The Apple Generic Memory Subsystem Model
• 4.1 Liveness Proof with Lemmas
• 4.2 Lemma-Free Proof of Liveness
• 5 Conclusions and Future Work
• A Soundness proofs
• References
• Software Verification
• Strided Difference Bound Matrices
• 1 Introduction and Motivation
• 2 DBMs, SDBMs, and HSDBMs
• 3 Satisfiability
• 3.1 GCD-Tightening Constraints
• 3.2 Satisfiability for HSDBMs in O(n4) Time
• 3.3 Satisfiability for SDBMs in O(n m Dlcm) Time
• 4 HSDBM Normalization
• 5 Operations for Abstract Interpretation
• 6 Empirical Study.
• 6.1 Methodology
• 6.2 Prevalence of SDBMs
• 6.3 Applications to Translation Validation
• 7 Related Work
• 8 Conclusion
• References
• The Top-Down Solver Verified: Building Confidence in Static Analyzers
• 1 Introduction
• 2 Preliminaries
• 3 The Plain Top-Down Solver
• 4 The Top-Down Solver
• 5 Related Work
• 6 Conclusion
• References
• End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT
• 1 Introduction
• 1.1 Challenges
• 1.2 Contributions
• 2 Preliminaries
• 3 A Workflow for End-to-End Refinement
• 3.1 Methodology
• 3.2 Application to a rBPF Virtual Machine
• 4 Symbolic CompCert ARM Interpreter
• 5 A Verified Just-In-Time Compiler for rBPF
• 5.1 JIT Design
• 5.2 JIT Correctness
• 5.3 JIT Vertical Refinement
• 6 HAVM: A Hybrid Interpreter for rBPF
• 7 Evaluation: Case Study of RIOT's Femto-Containers
• 8 Lessons Learned
• 9 Related Works
• 10 Conclusion
• References
• A Framework for Debugging Automated Program Verification Proofs via Proof Actions
• 1 Introduction
• 2 Proof Debugging Considered Painful
• 2.1 Background on Automated Program Verification in Verus
• 2.2 Examples of Proof Debugging
• 2.3 Automated Proof Debugging with Proof Actions
• 2.4 Challenges with Automatic Code Transformation
• 3 ProofPlumber: An Extensible Proof Action Framework
• 3.1 ProofPlumber's API Design
• 3.2 ProofPlumber's Implementation
• 4 Evaluation
• 4.1 RQ1: Are proof actions expressive enough?
• 4.2 RQ2: Does ProofPlumber make it easy to write proof actions?
• 4.3 RQ3: Can proof actions reduce the verifier's TCB?
• 5 Limitations
• 6 Related Work and Conclusion
• References
• Verification Algorithms for Automated Separation Logic Verifiers
• 1 Introduction
• 2 Verification Algorithms
• 2.1 Viper Verification Language
• 2.2 Design Dimensions
• 2.3 Algorithms
• 3 Evaluation.
• 3.1 Implementations.