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

Saved in:
Bibliographic Details
Superior document:Lecture Notes in Computer Science Series ; v.14681
:
TeilnehmendeR:
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)
Tags: Add Tag
No Tags, Be the first to tag this record!
id 993687475904498
ctrlnum (CKB)33601052200041
(MiAaPQ)EBC31594178
(Au-PeEL)EBL31594178
(EXLCZ)9933601052200041
collection bib_alma
record_format marc
spelling Gurfinkel, Arie.
Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I.
1st ed.
Cham : Springer International Publishing AG, 2024.
©2024.
1 online resource (523 pages)
text txt rdacontent
computer c rdamedia
online resource cr rdacarrier
Lecture Notes in Computer Science Series ; v.14681
Description based on publisher supplied metadata and other sources.
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.
Ganesh, Vijay.
3-031-65626-1
Lecture Notes in Computer Science Series
language English
format eBook
author Gurfinkel, Arie.
spellingShingle Gurfinkel, Arie.
Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I.
Lecture Notes in Computer Science Series ;
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.
author_facet Gurfinkel, Arie.
Ganesh, Vijay.
author_variant a g ag
author2 Ganesh, Vijay.
author2_variant v g vg
author2_role TeilnehmendeR
author_sort Gurfinkel, Arie.
title Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I.
title_sub 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I.
title_full Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I.
title_fullStr Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I.
title_full_unstemmed Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I.
title_auth Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I.
title_new Computer Aided Verification :
title_sort computer aided verification : 36th international conference, cav 2024, montreal, qc, canada, july 24-27, 2024, proceedings, part i.
series Lecture Notes in Computer Science Series ;
series2 Lecture Notes in Computer Science Series ;
publisher Springer International Publishing AG,
publishDate 2024
physical 1 online resource (523 pages)
edition 1st ed.
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.
isbn 3-031-65627-X
3-031-65626-1
callnumber-first Q - Science
callnumber-subject QA - Mathematics
callnumber-label QA76
callnumber-sort QA 276.758
illustrated Not Illustrated
work_keys_str_mv AT gurfinkelarie computeraidedverification36thinternationalconferencecav2024montrealqccanadajuly24272024proceedingsparti
AT ganeshvijay computeraidedverification36thinternationalconferencecav2024montrealqccanadajuly24272024proceedingsparti
status_str n
ids_txt_mv (CKB)33601052200041
(MiAaPQ)EBC31594178
(Au-PeEL)EBL31594178
(EXLCZ)9933601052200041
carrierType_str_mv cr
hierarchy_parent_title Lecture Notes in Computer Science Series ; v.14681
is_hierarchy_title Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I.
container_title Lecture Notes in Computer Science Series ; v.14681
author2_original_writing_str_mv noLinkedField
_version_ 1809671915492605952
fullrecord <?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>11085nam a22004573i 4500</leader><controlfield tag="001">993687475904498</controlfield><controlfield tag="005">20240812084530.0</controlfield><controlfield tag="006">m o d | </controlfield><controlfield tag="007">cr |||||||||||</controlfield><controlfield tag="008">240812s2024 xx o ||||0 eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">3-031-65627-X</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(CKB)33601052200041</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(MiAaPQ)EBC31594178</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(Au-PeEL)EBL31594178</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(EXLCZ)9933601052200041</subfield></datafield><datafield tag="040" ind1=" " ind2=" "><subfield code="a">MiAaPQ</subfield><subfield code="b">eng</subfield><subfield code="e">rda</subfield><subfield code="e">pn</subfield><subfield code="c">MiAaPQ</subfield><subfield code="d">MiAaPQ</subfield></datafield><datafield tag="050" ind1=" " ind2="4"><subfield code="a">QA76.758</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Gurfinkel, Arie.</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">Computer Aided Verification :</subfield><subfield code="b">36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I.</subfield></datafield><datafield tag="250" ind1=" " ind2=" "><subfield code="a">1st ed.</subfield></datafield><datafield tag="264" ind1=" " ind2="1"><subfield code="a">Cham :</subfield><subfield code="b">Springer International Publishing AG,</subfield><subfield code="c">2024.</subfield></datafield><datafield tag="264" ind1=" " ind2="4"><subfield code="c">©2024.</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (523 pages)</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="490" ind1="1" ind2=" "><subfield code="a">Lecture Notes in Computer Science Series ;</subfield><subfield code="v">v.14681</subfield></datafield><datafield tag="588" ind1=" " ind2=" "><subfield code="a">Description based on publisher supplied metadata and other sources.</subfield></datafield><datafield tag="505" ind1="0" ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">3.1 Implementations.</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Ganesh, Vijay.</subfield></datafield><datafield tag="776" ind1=" " ind2=" "><subfield code="z">3-031-65626-1</subfield></datafield><datafield tag="830" ind1=" " ind2="0"><subfield code="a">Lecture Notes in Computer Science Series</subfield></datafield><datafield tag="906" ind1=" " ind2=" "><subfield code="a">BOOK</subfield></datafield><datafield tag="ADM" ind1=" " ind2=" "><subfield code="b">2024-09-09 00:20:51 Europe/Vienna</subfield><subfield code="f">System</subfield><subfield code="c">marc21</subfield><subfield code="a">2024-08-04 11:53:47 Europe/Vienna</subfield><subfield code="g">false</subfield></datafield><datafield tag="AVE" ind1=" " ind2=" "><subfield code="i">DOAB Directory of Open Access Books</subfield><subfield code="P">DOAB Directory of Open Access Books</subfield><subfield code="x">https://eu02.alma.exlibrisgroup.com/view/uresolver/43ACC_OEAW/openurl?u.ignore_date_coverage=true&amp;portfolio_pid=5357522560004498&amp;Force_direct=true</subfield><subfield code="Z">5357522560004498</subfield><subfield code="b">Available</subfield><subfield code="8">5357522560004498</subfield></datafield></record></collection>