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.