Computer Aided Verification : : 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II.
Saved in:
Superior document: | Lecture Notes in Computer Science Series ; v.13965 |
---|---|
: | |
TeilnehmendeR: | |
Place / Publishing House: | Cham : : Springer,, 2023. ©2023. |
Year of Publication: | 2023 |
Edition: | 1st ed. |
Language: | English |
Series: | Lecture Notes in Computer Science Series
|
Online Access: | |
Physical Description: | 1 online resource (472 pages) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
LEADER | 11165nam a22004693i 4500 | ||
---|---|---|---|
001 | 50030651911 | ||
003 | MiAaPQ | ||
005 | 20240229073851.0 | ||
006 | m o d | | ||
007 | cr cnu|||||||| | ||
008 | 240229s2023 xx o ||||0 eng d | ||
020 | |a 9783031377037 |q (electronic bk.) | ||
020 | |z 9783031377020 | ||
035 | |a (MiAaPQ)50030651911 | ||
035 | |a (Au-PeEL)EBL30651911 | ||
035 | |a (OCoLC)1391143757 | ||
040 | |a MiAaPQ |b eng |e rda |e pn |c MiAaPQ |d MiAaPQ | ||
050 | 4 | |a QA76.758 | |
100 | 1 | |a Enea, Constantin. | |
245 | 1 | 0 | |a Computer Aided Verification : |b 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II. |
250 | |a 1st ed. | ||
264 | 1 | |a Cham : |b Springer, |c 2023. | |
264 | 4 | |c ©2023. | |
300 | |a 1 online resource (472 pages) | ||
336 | |a text |b txt |2 rdacontent | ||
337 | |a computer |b c |2 rdamedia | ||
338 | |a online resource |b cr |2 rdacarrier | ||
490 | 1 | |a Lecture Notes in Computer Science Series ; |v v.13965 | |
505 | 0 | |a 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. | |
505 | 8 | |a 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. | |
505 | 8 | |a 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. | |
505 | 8 | |a 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. | |
505 | 8 | |a 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. | |
505 | 8 | |a QEBVerif: Quantization Error Bound Verification of Neural Networks. | |
588 | |a Description based on publisher supplied metadata and other sources. | ||
590 | |a Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. | ||
655 | 4 | |a Electronic books. | |
700 | 1 | |a Lal, Akash. | |
776 | 0 | 8 | |i Print version: |a Enea, Constantin |t Computer Aided Verification |d Cham : Springer,c2023 |z 9783031377020 |
797 | 2 | |a ProQuest (Firm) | |
830 | 0 | |a Lecture Notes in Computer Science Series | |
856 | 4 | 0 | |u https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=30651911 |z Click to View |