Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24–27, 2024, Proceedings, Part I / edited by Arie Gurfinkel, Vijay Ganesh.

Format:

Book

Author/Creator:

Gurfinkel, Arie.

Contributor:

Ganesh, Vijay.

Series:

Lecture Notes in Computer Science, 1611-3349 ; 14681

Language:

English

Subjects (All):

Software engineering.

Artificial intelligence.

Algorithms.

Software Engineering.

Artificial Intelligence.

Design and Analysis of Algorithms.

Local Subjects:

Software Engineering.

Artificial Intelligence.

Design and Analysis of Algorithms.

Physical Description:

1 online resource (523 pages)

Edition:

1st ed. 2024.

Place of Publication:

Cham : Springer Nature Switzerland : Imprint: Springer, 2024.

Summary:

This open access book constitutes the proceedings of the 36th International Conference on Computer-Aided Verification, CAV 2024, which took place in Montreal, Canada, during July 24–27, 2024.

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

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

Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic

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

Distributed SMT Solving Based on Dynamic Variable-Level Partitioning

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

Quantified Linear Arithmetic Satisfiability via Fine-Grained Strategy Improvement

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

From Clauses to Klauses*

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.1 SAT Competition Benchmarks

7.2 Magic Squares and Max Squares

8 Conclusion and Future Work

CaDiCaL 2.0

2 Architecture

3 External Propagator

4 Proofs

5 Tracer Interface

6 Constraints and Flipping

7 Interpolation

8 Testing and Debugging

9 Experiments

10 Conclusion

Formally Certified Approximate Model Counting

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

Scalable Bit-Blasting with Abstractions

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

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

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

Avoiding the Shoals - A New Approach to Liveness Checking

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.1 Experimental Setup

5.2 Experimental Results

6 Conclusions

Toward Liveness Proofs at Scale

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

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

The Top-Down Solver Verified: Building Confidence in Static Analyzers

3 The Plain Top-Down Solver

4 The Top-Down Solver

5 Related Work

6 Conclusion

End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT

1.1 Challenges

1.2 Contributions

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

A Framework for Debugging Automated Program Verification Proofs via Proof Actions

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

Verification Algorithms for Automated Separation Logic Verifiers

2 Verification Algorithms

2.1 Viper Verification Language

2.2 Design Dimensions

2.3 Algorithms

3 Evaluation.

3.1 Implementations.

ISBN:

3-031-65627-X