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

The open access proceedings set LNCS 13964, 13965, 13966 constitutes the refereed proceedings of the 35th International Conference on Computer Aided Verification, CAV 2023, which was held in Paris, France, in July 2023.

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< -- 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 < -- 2-1 -- D.2 Proof of Pr[L] 0.085 for 1< -- 3 -- D.3 Proof of Pr[L] 0.055 for 3< -- 42-1 -- D.4 Proof of Pr[L] 0.023 for 42-1 -- D.5 Proof of Pr[U] 0.169 for < -- 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.