Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part II (Lecture Notes in Computer Science)

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. The 67 full papers presented in these proceedings were carefully reviewed and selected from 261 submissions. The have been organized in topical sections as follows: Part I: Automata and logic; concurrency; cyber-physical and hybrid systems; synthesis; Part II: Decision procedures; model checking; neural networks and machine learning; Part II: Probabilistic systems; security and quantum systems; software verification. 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