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.