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

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.

Detalles Bibliográficos
Autor principal:	Gurfinkel, Arie (-)
Otros Autores:	Ganesh, Vijay
Formato:	Libro electrónico
Idioma:	Inglés
Publicado:	Cham : Springer Nature Switzerland 2024.
Edición:	1st ed. 2024.
Colección:	Lecture Notes in Computer Science, 14681
Materias:	Software engineering. Artificial intelligence. Algorithms. Software Engineering. Artificial Intelligence. Design and Analysis of Algorithms.
Ver en Biblioteca Universitat Ramon Llull:	https://discovery.url.edu/permalink/34CSUC_URL/1im36ta/alma991009845837906719

Tabla de Contenidos:

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.

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

Ejemplares similares