| Description |
1 online resource (xvi, 460 pages) : illustrations (some color) |
| Series |
Lecture notes in computer science, 1611-3349 ; 13965 |
|
Lecture notes in computer science ; 13965. 1611-3349
|
| 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 |
| Summary |
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 |
| Notes |
Includes author index |
|
Online resource; title from PDF title page (SpringerLink, viewed July 26, 2023) |
| Subject |
Computer software -- Verification -- Congresses
|
|
Computer software -- Verification.
|
| Genre/Form |
Electronic books
|
|
proceedings (reports)
|
|
Conference papers and proceedings.
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Enea, Constantin, editor.
|
|
Lal, Akash, editor.
|
| ISBN |
9783031377037 |
|
3031377036 |
|
