Computer Aided Verification : : 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II.

• Superior document: Lecture Notes in Computer Science Series ; v.13965
• Author: Enea, Constantin.
• TeilnehmendeR: Lal, Akash.
• Place / Publishing House: Cham : : Springer,, 2023.; ©2023.
• Year of Publication: 2023
• Edition: 1st ed.
• Language: English
• Series: Lecture Notes in Computer Science Series
• Physical Description: 1 online resource (472 pages)

Table of Contents

• Intro
• Preface
• Organization
• Contents - Part II
• Decision Procedures
• Bitwuzla
• 1 Introduction
• 2 Architecture
• 2.1 Node Manager
• 2.2 Solving Context
• 3 Theory Solvers
• 3.1 Arrays
• 3.2 Bit-Vectors
• 3.3 Floating-Point Arithmetic
• 3.4 Uninterpreted Functions
• 3.5 Quantifiers
• 4 Evaluation
• 5 Conclusion
• References
• Decision Procedures for Sequence Theories
• 1 Introduction
• 2 Motivating Example
• 3 Models
• 4 Solving Equational and Regular Constraints
• 5 Algorithm for Straight-Line Formulas
• 6 Extensions and Undecidability
• 7 Implementations, Optimizations and Benchmarks
• 8 Conclusion and Future Work
• References
• Exploiting Adjoints in Property Directed Reachability Analysis
• 1 Introduction
• 2 Preliminaries and Notation
• 3 Adjoint PDR
• 3.1 Progression
• 3.2 Heuristics
• 3.3 Negative Termination
• 4 Recovering Adjoints with Lower Sets
• 4.1 AdjointPDR"3223379 : Positive Chain in L, Negative Sequence in L"3223379
• 4.2 AdjointPDR"3223379 Simulates LT-PDR
• 5 Instantiating AdjointPDR"3223379 for MDPs
• 6 Implementation and Experiments
• References
• Fast Approximations of Quantifier Elimination
• 1 Introduction
• 2 Background
• 3 Extracting Formulas from Egraphs
• 4 Quantifier Reduction
• 5 Model Based Projection Using QEL
• 6 Evaluation
• 7 Conclusion
• References
• Local Search for Solving Satisfiability of Polynomial Formulas
• 1 Introduction
• 2 Preliminaries
• 2.1 Notation
• 2.2 A General Local Search Framework
• 3 The Search Space of SMT(NRA)
• 4 The Cell-Jump Operation
• 4.1 Sample Points
• 4.2 Cell-Jump Along a Line Parallel to a Coordinate Axis
• 4.3 Cell-Jump Along a Fixed Straight Line
• 5 Scoring Functions
• 6 The Main Algorithm
• 7 Experiments
• 7.1 Experiment Preparation
• 7.2 Instances
• 7.3 Experimental Results
• 8 Conclusion.
• References
• Partial Quantifier Elimination and Property Generation
• 1 Introduction
• 2 Basic Definitions
• 3 Property Generation by PQE
• 3.1 High-Level View of Property Generation by PQE
• 3.2 Property Generation as Generalization of Testing
• 3.3 Computing Properties Efficiently
• 3.4 Using Design Coverage for Generation of Unwanted Properties
• 3.5 High-Quality Tests Specified by a Property Generated by PQE
• 4 Invariant Generation by PQE
• 4.1 Bugs Making States Unreachable
• 4.2 Proving Operative State Unreachability by Invariant Generation
• 5 Introducing EG-PQE
• 5.1 An Example
• 5.2 Description of EG-PQE
• 5.3 Discussion
• 6 Introducing EG-PQE+
• 6.1 Main Idea
• 6.2 Discussion
• 7 Experiment with FIFO Buffers
• 7.1 Buffer Description
• 7.2 Bug Detection by Invariant Generation
• 7.3 Detection of the Bug by Conventional Methods
• 8 Experiments with HWMCC Benchmarks
• 8.1 Experiment 1
• 8.2 Experiment 2
• 8.3 Experiment 3
• 9 Properties Mimicking Symbolic Simulation
• 10 Some Background
• 11 Conclusions and Directions for Future Research
• References
• Rounding Meets Approximate Model Counting
• 1 Introduction
• 2 Notation and Preliminaries
• 2.1 Universal Hash Functions
• 2.2 Helpful Combinatorial Inequality
• 3 Related Work
• 4 Weakness of ApproxMC
• 5 Rounding Model Counting
• 5.1 Algorithm
• 5.2 Repetition Reduction
• 5.3 Proof of Lemma 4 for Case 2-1&lt
• 1
• 6 Experimental Evaluation
• 6.1 RQ1. Overall Performance
• 6.2 RQ2. Approximation Quality
• 7 Conclusion
• A Proof of Proposition 1
• B Weakness of Proposition 3
• C Proof of pmax 0.36 for ApproxMC
• D Proof of Lemma 4
• D.1 Proof of Pr[L] 0.262 for &lt
• 2-1
• D.2 Proof of Pr[L] 0.085 for 1&lt
• 3
• D.3 Proof of Pr[L] 0.055 for 3&lt
• 42-1
• D.4 Proof of Pr[L] 0.023 for 42-1
• D.5 Proof of Pr[U] 0.169 for &lt
• 3.
• D.6 Proof of Pr[U] 0.044 for 3
• References
• Satisfiability Modulo Finite Fields
• 1 Introduction
• 1.1 Related Work
• 2 Background
• 2.1 Algebra
• 2.2 Ideal Membership
• 2.3 Zero Knowledge Proofs
• 2.4 SMT
• 3 The Theory of Finite Fields
• 4 Decision Procedure
• 4.1 Algebraic Reduction
• 4.2 Incomplete Unsatisfiability and Cores
• 4.3 Completeness Through Model Construction
• 5 Implementation
• 6 Benchmark Generation
• 6.1 Examples
• 7 Experiments
• 7.1 Comparison with Bit-Vectors
• 7.2 The Cost of Field Polynomials
• 7.3 The Benefit of UNSAT Cores
• 7.4 Comparison to Pure Computer Algebra
• 7.5 Main Experiment
• 8 Discussion and Future Work
• A Proofs of IdealCalc Properties
• B Proof of Correctness for FindZero
• C Benchmark Generation
• References
• Solving String Constraints Using SAT
• 1 Introduction
• 2 Preliminaries
• 3 Overview
• 4 Reducing the Alphabet
• 5 Propositional Encodings
• 5.1 Substitutions
• 5.2 Theory Literals
• 6 Refining Upper Bounds
• 6.1 Unsatisfiable-Core Analysis
• 7 Implementation
• 8 Experimental Evaluation
• 9 Conclusion
• References
• The GOLEM Horn Solver
• 1 Introduction
• 2 Tool Overview
• 3 Back-end Engines of GOLEM
• 3.1 Transition Power Abstraction
• 3.2 Engines for State-of-the-Art Model-Checking Algorithms
• 4 Experiments
• 4.1 Category LRA-TS
• 4.2 Category LIA-Lin
• 4.3 Category LIA-Nonlin
• 5 Conclusion
• References
• Model Checking
• CoqCryptoLine: A Verified Model Checker with Certified Results
• 1 Introduction
• 2 CoqCryptoLine
• 2.1 CryptoLine Language
• 2.2 The Architecture of CoqCryptoLine
• 2.3 Features and Optimizations
• 3 Walkthrough
• 4 Evaluation
• 5 Conclusion
• References
• Incremental Dead State Detection in Logarithmic Time
• 1 Introduction
• 2 Guided Incremental Digraphs
• 2.1 Problem Statement.
• 2.2 Existing Approaches
• 3 Algorithms
• 3.1 First-Cut Algorithm
• 3.2 Logarithmic Algorithm
• 3.3 Lazy Algorithm
• 4 Experimental Evaluation
• 5 Application to Extended Regular Expressions
• 5.1 Reduction from Incremental Regex Emptiness to GIDs
• 6 Related Work
• References
• Model Checking Race-Freedom When ``Sequential Consistency for Data-Race-Free Programs'' is Guaranteed
• 1 Introduction
• 2 Theory
• 3 Implementation and Evaluation
• 3.1 Background on OpenMP
• 3.2 Background on CIVL-C
• 3.3 Transformation for Data Race Detection
• 3.4 Evaluation
• 4 Related Work
• 5 Conclusion
• References
• Searching for i-Good Lemmas to Accelerate Safety Model Checking
• 1 Introduction
• 2 Preliminaries
• 2.1 Boolean Transition System
• 2.2 Safety Checking and Reachability Analysis
• 2.3 Overview of IC3 and CAR
• 3 Finding i-Good Lemmas
• 3.1 What Are i-good Lemmas
• 3.2 Searching for i-good Lemmas
• 4 Related Work
• 5 Evaluation
• 5.1 Experimental Setup
• 5.2 Experimental Results
• 5.3 Why Do branching and refer-skipping Work?
• 6 Conclusions and Future Work
• References
• Second-Order Hyperproperties
• 1 Introduction
• 2 Preliminaries
• 3 Second-Order HyperLTL
• 3.1 Hyper2LTL
• 3.2 Hyper2LTLfp
• 3.3 Common Knowledge in Multi-agent Systems
• 3.4 Hyper2LTL Model Checking
• 4 Expressiveness of Hyper2LTL
• 4.1 Hyper2LTL and LTLK, C
• 4.2 Hyper2LTL and Asynchronous Hyperproperties
• 5 Model-Checking Hyper2LTLfp
• 5.1 Fixpoints in Hyper2LTLfp
• 5.2 Functions as Automata
• 5.3 Model Checking for First-Order Quantification
• 5.4 Bidirectional Model Checking
• 5.5 Computing Under- and Overapproximations
• 6 Implementation and Experiments
• 7 Related Work
• 8 Conclusion
• References
• Neural Networks and Machine Learning
• Certifying the Fairness of KNN in the Presence of Dataset Bias
• 1 Introduction.
• 2 Background
• 2.1 Fairness of the Learned Model
• 2.2 Fairness in the Presence of Dataset Bias
• 3 Overview of Our Method
• 3.1 The KNN Algorithm
• 3.2 Certifying the KNN Algorithm
• 4 Abstracting the KNN Prediction Step
• 4.1 Finding the K-Nearest Neighbors
• 4.2 Checking the Classification Result
• 5 Abstracting the KNN Learning Step
• 5.1 Overapproximating the Classification Error
• 5.2 Underapproximating the Classification Error
• 6 Experiments
• 7 Related Work
• 8 Conclusions
• References
• Monitoring Algorithmic Fairness
• 1 Introduction
• 1.1 Motivating Examples
• 1.2 Related Work
• 2 Preliminaries
• 2.1 Markov Chains as Randomized Generators of Events
• 2.2 Randomized Register Monitors
• 3 Algorithmic Fairness Specifications and Problem Formulation
• 3.1 Probabilistic Specification Expressions
• 3.2 The Monitoring Problem
• 4 Frequentist Monitoring
• 4.1 The Main Principle
• 4.2 Implementation of the Frequentist Monitor
• 5 Bayesian Monitoring
• 5.1 The Main Principle
• 5.2 Implementation of the Bayesian Monitor
• 6 Experiments
• 7 Conclusion
• References
• nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
• 1 Introduction
• 2 Background and Related Work
• 2.1 Natural Language to Linear-Time Temporal Logic
• 2.2 Large Language Models
• 3 The nl2spec Framework
• 3.1 Overview
• 3.2 Interactive Few-Shot Prompting
• 4 Evaluation
• 4.1 Study Setup
• 4.2 Results
• 5 Conclusion
• References
• NNV 2.0: The Neural Network Verification Tool
• 1 Introduction
• 2 Related Work
• 3 Overview and Features
• 3.1 NNV 2.0 vs NNV
• 4 Evaluation
• 4.1 Comparison to MATLAB's Deep Learning Verification Toolbox
• 4.2 Neural Ordinary Differential Equations
• 4.3 Recurrent Neural Networks
• 4.4 Semantic Segmentation
• 5 Conclusions
• References.
• QEBVerif: Quantization Error Bound Verification of Neural Networks.