Computer Aided Verification : : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II.
Saved in:
Superior document: | Lecture Notes in Computer Science Series ; v.12760 |
---|---|
: | |
TeilnehmendeR: | |
Place / Publishing House: | Cham : : Springer International Publishing AG,, 2021. ©2021. |
Year of Publication: | 2021 |
Edition: | 1st ed. |
Language: | English |
Series: | Lecture Notes in Computer Science Series
|
Online Access: | |
Physical Description: | 1 online resource (955 pages) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
5006679368 |
---|---|
ctrlnum |
(MiAaPQ)5006679368 (Au-PeEL)EBL6679368 (OCoLC)1261897041 |
collection |
bib_alma |
record_format |
marc |
spelling |
Silva, Alexandra. Computer Aided Verification : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. 1st ed. Cham : Springer International Publishing AG, 2021. ©2021. 1 online resource (955 pages) text txt rdacontent computer c rdamedia online resource cr rdacarrier Lecture Notes in Computer Science Series ; v.12760 Intro -- Preface -- Organization -- Contents - Part II -- Contents - Part I -- Complexity and Termination -- Learning Probabilistic Termination Proofs -- 1 Introduction -- 2 Termination Analysis of Probabilistic Programs -- 3 Training Neural Ranking Supermartingales -- 4 Verifying Ranking Supermartingales by SMT Solving -- 4.1 From Programs to Symbolic Store Trees -- 4.2 Marginalisation -- 5 Case Studies -- 5.1 Non-linear Program Expressions and NRSMs -- 5.2 Multivariate and Hierarchical Distributions -- 5.3 State-Dependent Distributions and Non-Linear Expectations -- 5.4 Undefined Moments -- 5.5 Rare Transitions -- 6 Experimental Results -- 7 Conclusion -- References -- Ghost Signals: Verifying Termination of Busy Waiting -- 1 Introduction -- 2 A Guide on Verifying Termination of Busy Waiting -- 2.1 Simplest Setting: Thread-Safe Physical Signals -- 2.2 Non-Thread-Safe Physical Signals -- 2.3 Arbitrary Data Structures -- 2.4 Signal Erasure -- 3 A Realistic Example -- 4 Specifying Busy-Waiting Concurrent Objects -- 5 Tool Support -- 6 Integrating Higher-Order Features -- 7 Related and Future Work -- 8 Conclusion -- References -- Reflections on Termination of Linear Loops -- 1 Introduction -- 2 Preliminaries -- 2.1 Transition Systems -- 3 Linear Abstractions of Transition Formulas -- 3.1 Affine Abstractions of Transition Formulas -- 3.2 Reflections via the Dual Space -- 3.3 Determinization -- 3.4 Rational-Spectrum Reflections of DATS -- 4 Asymptotic Analysis of Linear Dynamical Systems -- 5 A Conditional Termination Analysis for Programs -- 6 Evaluation -- 7 Related Work -- References -- Decision Tree Learning in CEGIS-Based Termination Analysis -- 1 Introduction -- 2 Preview by Examples -- 2.1 Termination Verification by CEGIS -- 2.2 Handling Cycles in Decision Tree Learning -- 3 (Non-)Termination Verification as Constraint Solving. 4 CounterExample-Guided Inductive Synthesis (CEGIS) -- 5 Ranking Function Synthesis -- 5.1 Basic Definitions -- 5.2 Segmentation and (Explicit and Implicit) Cycles: One-Dimensional Case -- 5.3 Segmentation and (Explicit and Implicit) Cycles: Multi-Dimensional Lexicographic Case -- 5.4 Our Decision Tree Learning Algorithm -- 5.5 Improvement by Degenerating Negative Values -- 6 Implementation and Evaluation -- 7 Related Work -- 8 Conclusions and Future Work -- References -- ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures -- 1 Introduction -- 2 Step by Step to an Automated Analysis of Splaying -- 3 Technical Foundation -- 4 The Road to Automation, Continued -- 4.1 Type Checking -- 4.2 Type Inference -- 5 Implementation -- 5.1 The Three Phases of ATLAS -- 5.2 Details on the Generation of the Constraint System -- 5.3 Optimisation -- 6 Evaluation -- 6.1 Automated Analysis of Splaying et al. -- 6.2 Experimental Results -- 7 Conclusion -- References -- Decision Procedures and Solvers -- Theory Exploration Powered by Deductive Synthesis -- 1 Introduction -- 2 Overview -- 3 Preliminaries -- 3.1 Term Rewriting Systems -- 3.2 Compact Representation Using Equality Graphs -- 4 Theory Synthesis -- 4.1 Term Generation -- 4.2 Conjecture Inference and Screening -- 4.3 Induction Prover -- 4.4 Looping Back -- 5 Evaluation -- 5.1 Evaluating Theory Exploration Quality -- 5.2 Efficacy to Automated Proving -- 6 Related Work -- 7 Conclusion -- References -- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver -- 1 Introduction -- 2 Methodology Overview -- 3 Preliminaries -- 4 Bit-Vector Theory -- 5 Theory for SMT QF_BV Queries -- 5.1 Syntax of SMT QF_BV Queries -- 5.2 Semantics of SMT QF_BV Queries -- 5.3 Derived QF_BV Operations and Predicates -- 6 Certified Bit Blasting -- 7 A Certified SMT QF_BV Solver -- 8 Experiments. 8.1 SMT QF_BV Competition -- 8.2 Linear Field Arithmetic in Cryptography -- 9 Conclusion -- References -- Porous Invariants -- 1 Introduction -- 1.1 Related Work -- 2 Preliminaries -- 3 R Invariants: R-linear and R-semi-linear -- 4 Strongest Z-linear Invariants -- 4.1 Extensions of Z-linear Sets Without Strongest Invariants -- 4.2 Z-linear Targets -- 5 N-Semi-linear Invariants -- 5.1 Existence of Sufficient (but Non-minimal) N-semi-linear Invariants for Point Reachability in Deterministic LDS -- 5.2 Undecidability of N-semi-linear Invariants for Nondeterministic LDS -- 5.3 Nondeterministic One-Dimensional Affine Updates -- 6 The POROUS Tool -- 7 Conclusions and Open Directions -- References -- JavaSMT 3: Interacting with SMT Solvers in Java -- 1 Introduction -- 2 JavaSMT's Architecture and Solver Integration -- 3 New Contributions in JavaSMT 3 -- 4 Evaluation -- 5 Conclusion -- References -- Efficient SMT-Based Analysis of Failure Propagation -- 1 Introduction -- 2 Preliminaries -- 3 Propagation Graphs over FDSs -- 4 From Sequential to Combinational -- 5 Enumeration of FDS-Minimal Cut Sets -- 5.1 Algorithm for Boolean FDSs -- 5.2 Extension to Arbitrary FDSs -- 6 Related Work -- 6.1 Detailed Comparison with Finite Degradation Models -- 7 Experimental Evaluation -- 8 Conclusions and Further Work -- References -- ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends -- 1 Introduction -- 2 Detecting Failure-Inducing Inputs -- 3 Simplification Rules and Staged Simplification -- 4 Parsing and Input Representation -- 5 Delta Debugging Strategies -- 6 Experimental Evaluation -- 7 Conclusion -- References -- Learning Union of Integer Hypercubes with Queries -- 1 Introduction -- 2 Preliminaries -- 3 Minimally Adequate Teacher -- 3.1 Corner Oracle -- 3.2 Overshooting Algorithm -- 3.3 Repetition-Free Complexity -- 4 Extensions. 4.1 Maximal Cube Oracle -- 4.2 Maximal Cube Algorithm -- 4.3 Extension to the Infinite Case -- 4.4 Complexity -- 5 Applications and Experiments -- 5.1 Application to Monadic Decomposition -- 5.2 Experiments -- 5.3 Benchmark Suite -- 5.4 Results -- 6 Conclusion and Future Work -- References -- Interpolation and Model Checking for Nonlinear Arithmetic -- 1 Introduction -- 2 Background -- 3 SMT Modulo Models and Interpolation -- 3.1 Interpolation -- 3.2 SMT Modulo Models with MCSAT -- 4 Nonlinear Arithmetic -- 5 Evaluation -- 5.1 Related Work -- 6 Conclusion and Future Work -- References -- An SMT Solver for Regular Expressions and Linear Arithmetic over String Length -- 1 Introduction -- 2 Preliminaries -- 2.1 Basic Definitions -- 2.2 Theoretical Landscape -- 3 Length-Aware Regular Expression Algorithm -- 3.1 High-Level Algorithm -- 4 Length-Aware and Prefix/Suffix Heuristics in Z3str3RE -- 4.1 Computing Length Information from Regexes -- 4.2 Optimizing Automata Operations via Length Information -- 4.3 Leveraging Length Information to Optimize Search -- 4.4 Prefix/Suffix Over-Approximation Heuristic -- 5 Empirical Results -- 5.1 Empirical Setup and Solvers Used -- 5.2 Benchmarks -- 5.3 Comparison and Scoring Methods -- 5.4 Analysis of Empirical Results -- 5.5 Detailed Experimental Results -- 5.6 Analysis of Individual Heuristics and Results -- 6 Related Work -- 7 Conclusions and Future Work -- References -- Counting Minimal Unsatisfiable Subsets -- 1 Introduction -- 2 Preliminaries and Problem Definition -- 3 Related Work -- 4 MUS Counting via a Projected Model Counter -- 4.1 Basic MUS Counting Idea -- 4.2 W1 - the Base Wrapper and Its Reminder -- 4.3 W2 - the Intersection of MUSes -- 4.4 W3 - The Union of MUSes -- 4.5 W4 - Minimum MUS Cardinality -- 4.6 W5 - Maximum MUS Cardinality -- 4.7 W6 - Component Partitioning. 4.8 W7 - Minimal Hitting Set Duality -- 4.9 W8 - Literal Negation Cover -- 4.10 W9 - Non-extendable Evidence Models -- 4.11 W10 - Enforced Evidence Models -- 4.12 Combining Wrappers and Their Remainders -- 5 Experimental Evaluation -- 5.1 Solved Benchmarks -- 5.2 Scalability W.r.t the MUS Count -- 5.3 Accuracy of Wrappers -- 6 Future Possible Applications of Wrappers and Remainders -- 7 Conclusion and Future Work -- References -- Sound Verification Procedures for Temporal Properties of Infinite-State Systems -- 1 Introduction -- 2 The Cervino Language -- 2.1 Sorts, Relations and Axioms -- 2.2 Events -- 2.3 Commands -- 3 Background on FOLTL -- 3.1 Syntax and Semantics of FOLTL -- 3.2 Bounded Domain Property -- 3.3 Semantics of Cervino -- 4 Basic Transformations -- 4.1 Transforming Equality -- 4.2 Restricted Skolemization -- 4.3 Instantiation -- 4.4 Addressing Transitive Closure and the Between Relation -- 4.5 Geneva Transformation -- 5 TEA: Transforming Existential Quantifiers -- 6 TFC: Transforming Frame Conditions -- 7 TTC: Transforming Reflexive-Transitive Closure -- 8 Evaluation -- 9 Related Work -- 10 Conclusion -- References -- Hardware and Model Checking -- Progress in Certifying Hardware Model Checking Results -- 1 Introduction -- 2 Circuits -- 3 Model Checking -- 4 Certification -- 5 Implementation -- 6 Experiments -- 7 Conclusion -- References -- Model-Checking Structured Context-Free Languages -- 1 Introduction -- 2 Operator Precedence Languages -- 2.1 Operator Precedence Omega-Languages -- 2.2 Modeling Programs with OPA -- 3 POTL: Syntax and Semantics -- 3.1 Expressiveness of POTL -- 4 Model Checking -- 4.1 Model Checking for Omega-Words -- 4.2 Complexity -- 5 Experimental Evaluation -- 6 Conclusions -- References -- Model Checking -Regular Properties with Decoupled Search -- 1 Introduction -- 2 Büchi Automata, Composition and Verification. 3 The Decoupled State Space for Composed NBAs. Description based on publisher supplied metadata and other sources. Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. Electronic books. Leino, K. Rustan M. Print version: Silva, Alexandra Computer Aided Verification Cham : Springer International Publishing AG,c2021 9783030816872 ProQuest (Firm) Lecture Notes in Computer Science Series https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6679368 Click to View |
language |
English |
format |
eBook |
author |
Silva, Alexandra. |
spellingShingle |
Silva, Alexandra. Computer Aided Verification : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Lecture Notes in Computer Science Series ; Intro -- Preface -- Organization -- Contents - Part II -- Contents - Part I -- Complexity and Termination -- Learning Probabilistic Termination Proofs -- 1 Introduction -- 2 Termination Analysis of Probabilistic Programs -- 3 Training Neural Ranking Supermartingales -- 4 Verifying Ranking Supermartingales by SMT Solving -- 4.1 From Programs to Symbolic Store Trees -- 4.2 Marginalisation -- 5 Case Studies -- 5.1 Non-linear Program Expressions and NRSMs -- 5.2 Multivariate and Hierarchical Distributions -- 5.3 State-Dependent Distributions and Non-Linear Expectations -- 5.4 Undefined Moments -- 5.5 Rare Transitions -- 6 Experimental Results -- 7 Conclusion -- References -- Ghost Signals: Verifying Termination of Busy Waiting -- 1 Introduction -- 2 A Guide on Verifying Termination of Busy Waiting -- 2.1 Simplest Setting: Thread-Safe Physical Signals -- 2.2 Non-Thread-Safe Physical Signals -- 2.3 Arbitrary Data Structures -- 2.4 Signal Erasure -- 3 A Realistic Example -- 4 Specifying Busy-Waiting Concurrent Objects -- 5 Tool Support -- 6 Integrating Higher-Order Features -- 7 Related and Future Work -- 8 Conclusion -- References -- Reflections on Termination of Linear Loops -- 1 Introduction -- 2 Preliminaries -- 2.1 Transition Systems -- 3 Linear Abstractions of Transition Formulas -- 3.1 Affine Abstractions of Transition Formulas -- 3.2 Reflections via the Dual Space -- 3.3 Determinization -- 3.4 Rational-Spectrum Reflections of DATS -- 4 Asymptotic Analysis of Linear Dynamical Systems -- 5 A Conditional Termination Analysis for Programs -- 6 Evaluation -- 7 Related Work -- References -- Decision Tree Learning in CEGIS-Based Termination Analysis -- 1 Introduction -- 2 Preview by Examples -- 2.1 Termination Verification by CEGIS -- 2.2 Handling Cycles in Decision Tree Learning -- 3 (Non-)Termination Verification as Constraint Solving. 4 CounterExample-Guided Inductive Synthesis (CEGIS) -- 5 Ranking Function Synthesis -- 5.1 Basic Definitions -- 5.2 Segmentation and (Explicit and Implicit) Cycles: One-Dimensional Case -- 5.3 Segmentation and (Explicit and Implicit) Cycles: Multi-Dimensional Lexicographic Case -- 5.4 Our Decision Tree Learning Algorithm -- 5.5 Improvement by Degenerating Negative Values -- 6 Implementation and Evaluation -- 7 Related Work -- 8 Conclusions and Future Work -- References -- ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures -- 1 Introduction -- 2 Step by Step to an Automated Analysis of Splaying -- 3 Technical Foundation -- 4 The Road to Automation, Continued -- 4.1 Type Checking -- 4.2 Type Inference -- 5 Implementation -- 5.1 The Three Phases of ATLAS -- 5.2 Details on the Generation of the Constraint System -- 5.3 Optimisation -- 6 Evaluation -- 6.1 Automated Analysis of Splaying et al. -- 6.2 Experimental Results -- 7 Conclusion -- References -- Decision Procedures and Solvers -- Theory Exploration Powered by Deductive Synthesis -- 1 Introduction -- 2 Overview -- 3 Preliminaries -- 3.1 Term Rewriting Systems -- 3.2 Compact Representation Using Equality Graphs -- 4 Theory Synthesis -- 4.1 Term Generation -- 4.2 Conjecture Inference and Screening -- 4.3 Induction Prover -- 4.4 Looping Back -- 5 Evaluation -- 5.1 Evaluating Theory Exploration Quality -- 5.2 Efficacy to Automated Proving -- 6 Related Work -- 7 Conclusion -- References -- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver -- 1 Introduction -- 2 Methodology Overview -- 3 Preliminaries -- 4 Bit-Vector Theory -- 5 Theory for SMT QF_BV Queries -- 5.1 Syntax of SMT QF_BV Queries -- 5.2 Semantics of SMT QF_BV Queries -- 5.3 Derived QF_BV Operations and Predicates -- 6 Certified Bit Blasting -- 7 A Certified SMT QF_BV Solver -- 8 Experiments. 8.1 SMT QF_BV Competition -- 8.2 Linear Field Arithmetic in Cryptography -- 9 Conclusion -- References -- Porous Invariants -- 1 Introduction -- 1.1 Related Work -- 2 Preliminaries -- 3 R Invariants: R-linear and R-semi-linear -- 4 Strongest Z-linear Invariants -- 4.1 Extensions of Z-linear Sets Without Strongest Invariants -- 4.2 Z-linear Targets -- 5 N-Semi-linear Invariants -- 5.1 Existence of Sufficient (but Non-minimal) N-semi-linear Invariants for Point Reachability in Deterministic LDS -- 5.2 Undecidability of N-semi-linear Invariants for Nondeterministic LDS -- 5.3 Nondeterministic One-Dimensional Affine Updates -- 6 The POROUS Tool -- 7 Conclusions and Open Directions -- References -- JavaSMT 3: Interacting with SMT Solvers in Java -- 1 Introduction -- 2 JavaSMT's Architecture and Solver Integration -- 3 New Contributions in JavaSMT 3 -- 4 Evaluation -- 5 Conclusion -- References -- Efficient SMT-Based Analysis of Failure Propagation -- 1 Introduction -- 2 Preliminaries -- 3 Propagation Graphs over FDSs -- 4 From Sequential to Combinational -- 5 Enumeration of FDS-Minimal Cut Sets -- 5.1 Algorithm for Boolean FDSs -- 5.2 Extension to Arbitrary FDSs -- 6 Related Work -- 6.1 Detailed Comparison with Finite Degradation Models -- 7 Experimental Evaluation -- 8 Conclusions and Further Work -- References -- ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends -- 1 Introduction -- 2 Detecting Failure-Inducing Inputs -- 3 Simplification Rules and Staged Simplification -- 4 Parsing and Input Representation -- 5 Delta Debugging Strategies -- 6 Experimental Evaluation -- 7 Conclusion -- References -- Learning Union of Integer Hypercubes with Queries -- 1 Introduction -- 2 Preliminaries -- 3 Minimally Adequate Teacher -- 3.1 Corner Oracle -- 3.2 Overshooting Algorithm -- 3.3 Repetition-Free Complexity -- 4 Extensions. 4.1 Maximal Cube Oracle -- 4.2 Maximal Cube Algorithm -- 4.3 Extension to the Infinite Case -- 4.4 Complexity -- 5 Applications and Experiments -- 5.1 Application to Monadic Decomposition -- 5.2 Experiments -- 5.3 Benchmark Suite -- 5.4 Results -- 6 Conclusion and Future Work -- References -- Interpolation and Model Checking for Nonlinear Arithmetic -- 1 Introduction -- 2 Background -- 3 SMT Modulo Models and Interpolation -- 3.1 Interpolation -- 3.2 SMT Modulo Models with MCSAT -- 4 Nonlinear Arithmetic -- 5 Evaluation -- 5.1 Related Work -- 6 Conclusion and Future Work -- References -- An SMT Solver for Regular Expressions and Linear Arithmetic over String Length -- 1 Introduction -- 2 Preliminaries -- 2.1 Basic Definitions -- 2.2 Theoretical Landscape -- 3 Length-Aware Regular Expression Algorithm -- 3.1 High-Level Algorithm -- 4 Length-Aware and Prefix/Suffix Heuristics in Z3str3RE -- 4.1 Computing Length Information from Regexes -- 4.2 Optimizing Automata Operations via Length Information -- 4.3 Leveraging Length Information to Optimize Search -- 4.4 Prefix/Suffix Over-Approximation Heuristic -- 5 Empirical Results -- 5.1 Empirical Setup and Solvers Used -- 5.2 Benchmarks -- 5.3 Comparison and Scoring Methods -- 5.4 Analysis of Empirical Results -- 5.5 Detailed Experimental Results -- 5.6 Analysis of Individual Heuristics and Results -- 6 Related Work -- 7 Conclusions and Future Work -- References -- Counting Minimal Unsatisfiable Subsets -- 1 Introduction -- 2 Preliminaries and Problem Definition -- 3 Related Work -- 4 MUS Counting via a Projected Model Counter -- 4.1 Basic MUS Counting Idea -- 4.2 W1 - the Base Wrapper and Its Reminder -- 4.3 W2 - the Intersection of MUSes -- 4.4 W3 - The Union of MUSes -- 4.5 W4 - Minimum MUS Cardinality -- 4.6 W5 - Maximum MUS Cardinality -- 4.7 W6 - Component Partitioning. 4.8 W7 - Minimal Hitting Set Duality -- 4.9 W8 - Literal Negation Cover -- 4.10 W9 - Non-extendable Evidence Models -- 4.11 W10 - Enforced Evidence Models -- 4.12 Combining Wrappers and Their Remainders -- 5 Experimental Evaluation -- 5.1 Solved Benchmarks -- 5.2 Scalability W.r.t the MUS Count -- 5.3 Accuracy of Wrappers -- 6 Future Possible Applications of Wrappers and Remainders -- 7 Conclusion and Future Work -- References -- Sound Verification Procedures for Temporal Properties of Infinite-State Systems -- 1 Introduction -- 2 The Cervino Language -- 2.1 Sorts, Relations and Axioms -- 2.2 Events -- 2.3 Commands -- 3 Background on FOLTL -- 3.1 Syntax and Semantics of FOLTL -- 3.2 Bounded Domain Property -- 3.3 Semantics of Cervino -- 4 Basic Transformations -- 4.1 Transforming Equality -- 4.2 Restricted Skolemization -- 4.3 Instantiation -- 4.4 Addressing Transitive Closure and the Between Relation -- 4.5 Geneva Transformation -- 5 TEA: Transforming Existential Quantifiers -- 6 TFC: Transforming Frame Conditions -- 7 TTC: Transforming Reflexive-Transitive Closure -- 8 Evaluation -- 9 Related Work -- 10 Conclusion -- References -- Hardware and Model Checking -- Progress in Certifying Hardware Model Checking Results -- 1 Introduction -- 2 Circuits -- 3 Model Checking -- 4 Certification -- 5 Implementation -- 6 Experiments -- 7 Conclusion -- References -- Model-Checking Structured Context-Free Languages -- 1 Introduction -- 2 Operator Precedence Languages -- 2.1 Operator Precedence Omega-Languages -- 2.2 Modeling Programs with OPA -- 3 POTL: Syntax and Semantics -- 3.1 Expressiveness of POTL -- 4 Model Checking -- 4.1 Model Checking for Omega-Words -- 4.2 Complexity -- 5 Experimental Evaluation -- 6 Conclusions -- References -- Model Checking -Regular Properties with Decoupled Search -- 1 Introduction -- 2 Büchi Automata, Composition and Verification. 3 The Decoupled State Space for Composed NBAs. |
author_facet |
Silva, Alexandra. Leino, K. Rustan M. |
author_variant |
a s as |
author2 |
Leino, K. Rustan M. |
author2_variant |
k r m l krm krml |
author2_role |
TeilnehmendeR |
author_sort |
Silva, Alexandra. |
title |
Computer Aided Verification : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. |
title_sub |
33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. |
title_full |
Computer Aided Verification : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. |
title_fullStr |
Computer Aided Verification : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. |
title_full_unstemmed |
Computer Aided Verification : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. |
title_auth |
Computer Aided Verification : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. |
title_new |
Computer Aided Verification : |
title_sort |
computer aided verification : 33rd international conference, cav 2021, virtual event, july 20-23, 2021, proceedings, part ii. |
series |
Lecture Notes in Computer Science Series ; |
series2 |
Lecture Notes in Computer Science Series ; |
publisher |
Springer International Publishing AG, |
publishDate |
2021 |
physical |
1 online resource (955 pages) |
edition |
1st ed. |
contents |
Intro -- Preface -- Organization -- Contents - Part II -- Contents - Part I -- Complexity and Termination -- Learning Probabilistic Termination Proofs -- 1 Introduction -- 2 Termination Analysis of Probabilistic Programs -- 3 Training Neural Ranking Supermartingales -- 4 Verifying Ranking Supermartingales by SMT Solving -- 4.1 From Programs to Symbolic Store Trees -- 4.2 Marginalisation -- 5 Case Studies -- 5.1 Non-linear Program Expressions and NRSMs -- 5.2 Multivariate and Hierarchical Distributions -- 5.3 State-Dependent Distributions and Non-Linear Expectations -- 5.4 Undefined Moments -- 5.5 Rare Transitions -- 6 Experimental Results -- 7 Conclusion -- References -- Ghost Signals: Verifying Termination of Busy Waiting -- 1 Introduction -- 2 A Guide on Verifying Termination of Busy Waiting -- 2.1 Simplest Setting: Thread-Safe Physical Signals -- 2.2 Non-Thread-Safe Physical Signals -- 2.3 Arbitrary Data Structures -- 2.4 Signal Erasure -- 3 A Realistic Example -- 4 Specifying Busy-Waiting Concurrent Objects -- 5 Tool Support -- 6 Integrating Higher-Order Features -- 7 Related and Future Work -- 8 Conclusion -- References -- Reflections on Termination of Linear Loops -- 1 Introduction -- 2 Preliminaries -- 2.1 Transition Systems -- 3 Linear Abstractions of Transition Formulas -- 3.1 Affine Abstractions of Transition Formulas -- 3.2 Reflections via the Dual Space -- 3.3 Determinization -- 3.4 Rational-Spectrum Reflections of DATS -- 4 Asymptotic Analysis of Linear Dynamical Systems -- 5 A Conditional Termination Analysis for Programs -- 6 Evaluation -- 7 Related Work -- References -- Decision Tree Learning in CEGIS-Based Termination Analysis -- 1 Introduction -- 2 Preview by Examples -- 2.1 Termination Verification by CEGIS -- 2.2 Handling Cycles in Decision Tree Learning -- 3 (Non-)Termination Verification as Constraint Solving. 4 CounterExample-Guided Inductive Synthesis (CEGIS) -- 5 Ranking Function Synthesis -- 5.1 Basic Definitions -- 5.2 Segmentation and (Explicit and Implicit) Cycles: One-Dimensional Case -- 5.3 Segmentation and (Explicit and Implicit) Cycles: Multi-Dimensional Lexicographic Case -- 5.4 Our Decision Tree Learning Algorithm -- 5.5 Improvement by Degenerating Negative Values -- 6 Implementation and Evaluation -- 7 Related Work -- 8 Conclusions and Future Work -- References -- ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures -- 1 Introduction -- 2 Step by Step to an Automated Analysis of Splaying -- 3 Technical Foundation -- 4 The Road to Automation, Continued -- 4.1 Type Checking -- 4.2 Type Inference -- 5 Implementation -- 5.1 The Three Phases of ATLAS -- 5.2 Details on the Generation of the Constraint System -- 5.3 Optimisation -- 6 Evaluation -- 6.1 Automated Analysis of Splaying et al. -- 6.2 Experimental Results -- 7 Conclusion -- References -- Decision Procedures and Solvers -- Theory Exploration Powered by Deductive Synthesis -- 1 Introduction -- 2 Overview -- 3 Preliminaries -- 3.1 Term Rewriting Systems -- 3.2 Compact Representation Using Equality Graphs -- 4 Theory Synthesis -- 4.1 Term Generation -- 4.2 Conjecture Inference and Screening -- 4.3 Induction Prover -- 4.4 Looping Back -- 5 Evaluation -- 5.1 Evaluating Theory Exploration Quality -- 5.2 Efficacy to Automated Proving -- 6 Related Work -- 7 Conclusion -- References -- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver -- 1 Introduction -- 2 Methodology Overview -- 3 Preliminaries -- 4 Bit-Vector Theory -- 5 Theory for SMT QF_BV Queries -- 5.1 Syntax of SMT QF_BV Queries -- 5.2 Semantics of SMT QF_BV Queries -- 5.3 Derived QF_BV Operations and Predicates -- 6 Certified Bit Blasting -- 7 A Certified SMT QF_BV Solver -- 8 Experiments. 8.1 SMT QF_BV Competition -- 8.2 Linear Field Arithmetic in Cryptography -- 9 Conclusion -- References -- Porous Invariants -- 1 Introduction -- 1.1 Related Work -- 2 Preliminaries -- 3 R Invariants: R-linear and R-semi-linear -- 4 Strongest Z-linear Invariants -- 4.1 Extensions of Z-linear Sets Without Strongest Invariants -- 4.2 Z-linear Targets -- 5 N-Semi-linear Invariants -- 5.1 Existence of Sufficient (but Non-minimal) N-semi-linear Invariants for Point Reachability in Deterministic LDS -- 5.2 Undecidability of N-semi-linear Invariants for Nondeterministic LDS -- 5.3 Nondeterministic One-Dimensional Affine Updates -- 6 The POROUS Tool -- 7 Conclusions and Open Directions -- References -- JavaSMT 3: Interacting with SMT Solvers in Java -- 1 Introduction -- 2 JavaSMT's Architecture and Solver Integration -- 3 New Contributions in JavaSMT 3 -- 4 Evaluation -- 5 Conclusion -- References -- Efficient SMT-Based Analysis of Failure Propagation -- 1 Introduction -- 2 Preliminaries -- 3 Propagation Graphs over FDSs -- 4 From Sequential to Combinational -- 5 Enumeration of FDS-Minimal Cut Sets -- 5.1 Algorithm for Boolean FDSs -- 5.2 Extension to Arbitrary FDSs -- 6 Related Work -- 6.1 Detailed Comparison with Finite Degradation Models -- 7 Experimental Evaluation -- 8 Conclusions and Further Work -- References -- ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends -- 1 Introduction -- 2 Detecting Failure-Inducing Inputs -- 3 Simplification Rules and Staged Simplification -- 4 Parsing and Input Representation -- 5 Delta Debugging Strategies -- 6 Experimental Evaluation -- 7 Conclusion -- References -- Learning Union of Integer Hypercubes with Queries -- 1 Introduction -- 2 Preliminaries -- 3 Minimally Adequate Teacher -- 3.1 Corner Oracle -- 3.2 Overshooting Algorithm -- 3.3 Repetition-Free Complexity -- 4 Extensions. 4.1 Maximal Cube Oracle -- 4.2 Maximal Cube Algorithm -- 4.3 Extension to the Infinite Case -- 4.4 Complexity -- 5 Applications and Experiments -- 5.1 Application to Monadic Decomposition -- 5.2 Experiments -- 5.3 Benchmark Suite -- 5.4 Results -- 6 Conclusion and Future Work -- References -- Interpolation and Model Checking for Nonlinear Arithmetic -- 1 Introduction -- 2 Background -- 3 SMT Modulo Models and Interpolation -- 3.1 Interpolation -- 3.2 SMT Modulo Models with MCSAT -- 4 Nonlinear Arithmetic -- 5 Evaluation -- 5.1 Related Work -- 6 Conclusion and Future Work -- References -- An SMT Solver for Regular Expressions and Linear Arithmetic over String Length -- 1 Introduction -- 2 Preliminaries -- 2.1 Basic Definitions -- 2.2 Theoretical Landscape -- 3 Length-Aware Regular Expression Algorithm -- 3.1 High-Level Algorithm -- 4 Length-Aware and Prefix/Suffix Heuristics in Z3str3RE -- 4.1 Computing Length Information from Regexes -- 4.2 Optimizing Automata Operations via Length Information -- 4.3 Leveraging Length Information to Optimize Search -- 4.4 Prefix/Suffix Over-Approximation Heuristic -- 5 Empirical Results -- 5.1 Empirical Setup and Solvers Used -- 5.2 Benchmarks -- 5.3 Comparison and Scoring Methods -- 5.4 Analysis of Empirical Results -- 5.5 Detailed Experimental Results -- 5.6 Analysis of Individual Heuristics and Results -- 6 Related Work -- 7 Conclusions and Future Work -- References -- Counting Minimal Unsatisfiable Subsets -- 1 Introduction -- 2 Preliminaries and Problem Definition -- 3 Related Work -- 4 MUS Counting via a Projected Model Counter -- 4.1 Basic MUS Counting Idea -- 4.2 W1 - the Base Wrapper and Its Reminder -- 4.3 W2 - the Intersection of MUSes -- 4.4 W3 - The Union of MUSes -- 4.5 W4 - Minimum MUS Cardinality -- 4.6 W5 - Maximum MUS Cardinality -- 4.7 W6 - Component Partitioning. 4.8 W7 - Minimal Hitting Set Duality -- 4.9 W8 - Literal Negation Cover -- 4.10 W9 - Non-extendable Evidence Models -- 4.11 W10 - Enforced Evidence Models -- 4.12 Combining Wrappers and Their Remainders -- 5 Experimental Evaluation -- 5.1 Solved Benchmarks -- 5.2 Scalability W.r.t the MUS Count -- 5.3 Accuracy of Wrappers -- 6 Future Possible Applications of Wrappers and Remainders -- 7 Conclusion and Future Work -- References -- Sound Verification Procedures for Temporal Properties of Infinite-State Systems -- 1 Introduction -- 2 The Cervino Language -- 2.1 Sorts, Relations and Axioms -- 2.2 Events -- 2.3 Commands -- 3 Background on FOLTL -- 3.1 Syntax and Semantics of FOLTL -- 3.2 Bounded Domain Property -- 3.3 Semantics of Cervino -- 4 Basic Transformations -- 4.1 Transforming Equality -- 4.2 Restricted Skolemization -- 4.3 Instantiation -- 4.4 Addressing Transitive Closure and the Between Relation -- 4.5 Geneva Transformation -- 5 TEA: Transforming Existential Quantifiers -- 6 TFC: Transforming Frame Conditions -- 7 TTC: Transforming Reflexive-Transitive Closure -- 8 Evaluation -- 9 Related Work -- 10 Conclusion -- References -- Hardware and Model Checking -- Progress in Certifying Hardware Model Checking Results -- 1 Introduction -- 2 Circuits -- 3 Model Checking -- 4 Certification -- 5 Implementation -- 6 Experiments -- 7 Conclusion -- References -- Model-Checking Structured Context-Free Languages -- 1 Introduction -- 2 Operator Precedence Languages -- 2.1 Operator Precedence Omega-Languages -- 2.2 Modeling Programs with OPA -- 3 POTL: Syntax and Semantics -- 3.1 Expressiveness of POTL -- 4 Model Checking -- 4.1 Model Checking for Omega-Words -- 4.2 Complexity -- 5 Experimental Evaluation -- 6 Conclusions -- References -- Model Checking -Regular Properties with Decoupled Search -- 1 Introduction -- 2 Büchi Automata, Composition and Verification. 3 The Decoupled State Space for Composed NBAs. |
isbn |
9783030816889 9783030816872 |
callnumber-first |
Q - Science |
callnumber-subject |
QA - Mathematics |
callnumber-label |
QA76 |
callnumber-sort |
QA 276.758 |
genre |
Electronic books. |
genre_facet |
Electronic books. |
url |
https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6679368 |
illustrated |
Not Illustrated |
oclc_num |
1261897041 |
work_keys_str_mv |
AT silvaalexandra computeraidedverification33rdinternationalconferencecav2021virtualeventjuly20232021proceedingspartii AT leinokrustanm computeraidedverification33rdinternationalconferencecav2021virtualeventjuly20232021proceedingspartii |
status_str |
n |
ids_txt_mv |
(MiAaPQ)5006679368 (Au-PeEL)EBL6679368 (OCoLC)1261897041 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Lecture Notes in Computer Science Series ; v.12760 |
is_hierarchy_title |
Computer Aided Verification : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. |
container_title |
Lecture Notes in Computer Science Series ; v.12760 |
author2_original_writing_str_mv |
noLinkedField |
marc_error |
Info : MARC8 translation shorter than ISO-8859-1, choosing MARC8. --- [ 856 : z ] |
_version_ |
1792331059910672385 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>11185nam a22004693i 4500</leader><controlfield tag="001">5006679368</controlfield><controlfield tag="003">MiAaPQ</controlfield><controlfield tag="005">20240229073842.0</controlfield><controlfield tag="006">m o d | </controlfield><controlfield tag="007">cr cnu||||||||</controlfield><controlfield tag="008">240229s2021 xx o ||||0 eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">9783030816889</subfield><subfield code="q">(electronic bk.)</subfield></datafield><datafield tag="020" ind1=" " ind2=" "><subfield code="z">9783030816872</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(MiAaPQ)5006679368</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(Au-PeEL)EBL6679368</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(OCoLC)1261897041</subfield></datafield><datafield tag="040" ind1=" " ind2=" "><subfield code="a">MiAaPQ</subfield><subfield code="b">eng</subfield><subfield code="e">rda</subfield><subfield code="e">pn</subfield><subfield code="c">MiAaPQ</subfield><subfield code="d">MiAaPQ</subfield></datafield><datafield tag="050" ind1=" " ind2="4"><subfield code="a">QA76.758</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Silva, Alexandra.</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">Computer Aided Verification :</subfield><subfield code="b">33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II.</subfield></datafield><datafield tag="250" ind1=" " ind2=" "><subfield code="a">1st ed.</subfield></datafield><datafield tag="264" ind1=" " ind2="1"><subfield code="a">Cham :</subfield><subfield code="b">Springer International Publishing AG,</subfield><subfield code="c">2021.</subfield></datafield><datafield tag="264" ind1=" " ind2="4"><subfield code="c">©2021.</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (955 pages)</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="490" ind1="1" ind2=" "><subfield code="a">Lecture Notes in Computer Science Series ;</subfield><subfield code="v">v.12760</subfield></datafield><datafield tag="505" ind1="0" ind2=" "><subfield code="a">Intro -- Preface -- Organization -- Contents - Part II -- Contents - Part I -- Complexity and Termination -- Learning Probabilistic Termination Proofs -- 1 Introduction -- 2 Termination Analysis of Probabilistic Programs -- 3 Training Neural Ranking Supermartingales -- 4 Verifying Ranking Supermartingales by SMT Solving -- 4.1 From Programs to Symbolic Store Trees -- 4.2 Marginalisation -- 5 Case Studies -- 5.1 Non-linear Program Expressions and NRSMs -- 5.2 Multivariate and Hierarchical Distributions -- 5.3 State-Dependent Distributions and Non-Linear Expectations -- 5.4 Undefined Moments -- 5.5 Rare Transitions -- 6 Experimental Results -- 7 Conclusion -- References -- Ghost Signals: Verifying Termination of Busy Waiting -- 1 Introduction -- 2 A Guide on Verifying Termination of Busy Waiting -- 2.1 Simplest Setting: Thread-Safe Physical Signals -- 2.2 Non-Thread-Safe Physical Signals -- 2.3 Arbitrary Data Structures -- 2.4 Signal Erasure -- 3 A Realistic Example -- 4 Specifying Busy-Waiting Concurrent Objects -- 5 Tool Support -- 6 Integrating Higher-Order Features -- 7 Related and Future Work -- 8 Conclusion -- References -- Reflections on Termination of Linear Loops -- 1 Introduction -- 2 Preliminaries -- 2.1 Transition Systems -- 3 Linear Abstractions of Transition Formulas -- 3.1 Affine Abstractions of Transition Formulas -- 3.2 Reflections via the Dual Space -- 3.3 Determinization -- 3.4 Rational-Spectrum Reflections of DATS -- 4 Asymptotic Analysis of Linear Dynamical Systems -- 5 A Conditional Termination Analysis for Programs -- 6 Evaluation -- 7 Related Work -- References -- Decision Tree Learning in CEGIS-Based Termination Analysis -- 1 Introduction -- 2 Preview by Examples -- 2.1 Termination Verification by CEGIS -- 2.2 Handling Cycles in Decision Tree Learning -- 3 (Non-)Termination Verification as Constraint Solving.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">4 CounterExample-Guided Inductive Synthesis (CEGIS) -- 5 Ranking Function Synthesis -- 5.1 Basic Definitions -- 5.2 Segmentation and (Explicit and Implicit) Cycles: One-Dimensional Case -- 5.3 Segmentation and (Explicit and Implicit) Cycles: Multi-Dimensional Lexicographic Case -- 5.4 Our Decision Tree Learning Algorithm -- 5.5 Improvement by Degenerating Negative Values -- 6 Implementation and Evaluation -- 7 Related Work -- 8 Conclusions and Future Work -- References -- ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures -- 1 Introduction -- 2 Step by Step to an Automated Analysis of Splaying -- 3 Technical Foundation -- 4 The Road to Automation, Continued -- 4.1 Type Checking -- 4.2 Type Inference -- 5 Implementation -- 5.1 The Three Phases of ATLAS -- 5.2 Details on the Generation of the Constraint System -- 5.3 Optimisation -- 6 Evaluation -- 6.1 Automated Analysis of Splaying et al. -- 6.2 Experimental Results -- 7 Conclusion -- References -- Decision Procedures and Solvers -- Theory Exploration Powered by Deductive Synthesis -- 1 Introduction -- 2 Overview -- 3 Preliminaries -- 3.1 Term Rewriting Systems -- 3.2 Compact Representation Using Equality Graphs -- 4 Theory Synthesis -- 4.1 Term Generation -- 4.2 Conjecture Inference and Screening -- 4.3 Induction Prover -- 4.4 Looping Back -- 5 Evaluation -- 5.1 Evaluating Theory Exploration Quality -- 5.2 Efficacy to Automated Proving -- 6 Related Work -- 7 Conclusion -- References -- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver -- 1 Introduction -- 2 Methodology Overview -- 3 Preliminaries -- 4 Bit-Vector Theory -- 5 Theory for SMT QF_BV Queries -- 5.1 Syntax of SMT QF_BV Queries -- 5.2 Semantics of SMT QF_BV Queries -- 5.3 Derived QF_BV Operations and Predicates -- 6 Certified Bit Blasting -- 7 A Certified SMT QF_BV Solver -- 8 Experiments.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">8.1 SMT QF_BV Competition -- 8.2 Linear Field Arithmetic in Cryptography -- 9 Conclusion -- References -- Porous Invariants -- 1 Introduction -- 1.1 Related Work -- 2 Preliminaries -- 3 R Invariants: R-linear and R-semi-linear -- 4 Strongest Z-linear Invariants -- 4.1 Extensions of Z-linear Sets Without Strongest Invariants -- 4.2 Z-linear Targets -- 5 N-Semi-linear Invariants -- 5.1 Existence of Sufficient (but Non-minimal) N-semi-linear Invariants for Point Reachability in Deterministic LDS -- 5.2 Undecidability of N-semi-linear Invariants for Nondeterministic LDS -- 5.3 Nondeterministic One-Dimensional Affine Updates -- 6 The POROUS Tool -- 7 Conclusions and Open Directions -- References -- JavaSMT 3: Interacting with SMT Solvers in Java -- 1 Introduction -- 2 JavaSMT's Architecture and Solver Integration -- 3 New Contributions in JavaSMT 3 -- 4 Evaluation -- 5 Conclusion -- References -- Efficient SMT-Based Analysis of Failure Propagation -- 1 Introduction -- 2 Preliminaries -- 3 Propagation Graphs over FDSs -- 4 From Sequential to Combinational -- 5 Enumeration of FDS-Minimal Cut Sets -- 5.1 Algorithm for Boolean FDSs -- 5.2 Extension to Arbitrary FDSs -- 6 Related Work -- 6.1 Detailed Comparison with Finite Degradation Models -- 7 Experimental Evaluation -- 8 Conclusions and Further Work -- References -- ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends -- 1 Introduction -- 2 Detecting Failure-Inducing Inputs -- 3 Simplification Rules and Staged Simplification -- 4 Parsing and Input Representation -- 5 Delta Debugging Strategies -- 6 Experimental Evaluation -- 7 Conclusion -- References -- Learning Union of Integer Hypercubes with Queries -- 1 Introduction -- 2 Preliminaries -- 3 Minimally Adequate Teacher -- 3.1 Corner Oracle -- 3.2 Overshooting Algorithm -- 3.3 Repetition-Free Complexity -- 4 Extensions.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">4.1 Maximal Cube Oracle -- 4.2 Maximal Cube Algorithm -- 4.3 Extension to the Infinite Case -- 4.4 Complexity -- 5 Applications and Experiments -- 5.1 Application to Monadic Decomposition -- 5.2 Experiments -- 5.3 Benchmark Suite -- 5.4 Results -- 6 Conclusion and Future Work -- References -- Interpolation and Model Checking for Nonlinear Arithmetic -- 1 Introduction -- 2 Background -- 3 SMT Modulo Models and Interpolation -- 3.1 Interpolation -- 3.2 SMT Modulo Models with MCSAT -- 4 Nonlinear Arithmetic -- 5 Evaluation -- 5.1 Related Work -- 6 Conclusion and Future Work -- References -- An SMT Solver for Regular Expressions and Linear Arithmetic over String Length -- 1 Introduction -- 2 Preliminaries -- 2.1 Basic Definitions -- 2.2 Theoretical Landscape -- 3 Length-Aware Regular Expression Algorithm -- 3.1 High-Level Algorithm -- 4 Length-Aware and Prefix/Suffix Heuristics in Z3str3RE -- 4.1 Computing Length Information from Regexes -- 4.2 Optimizing Automata Operations via Length Information -- 4.3 Leveraging Length Information to Optimize Search -- 4.4 Prefix/Suffix Over-Approximation Heuristic -- 5 Empirical Results -- 5.1 Empirical Setup and Solvers Used -- 5.2 Benchmarks -- 5.3 Comparison and Scoring Methods -- 5.4 Analysis of Empirical Results -- 5.5 Detailed Experimental Results -- 5.6 Analysis of Individual Heuristics and Results -- 6 Related Work -- 7 Conclusions and Future Work -- References -- Counting Minimal Unsatisfiable Subsets -- 1 Introduction -- 2 Preliminaries and Problem Definition -- 3 Related Work -- 4 MUS Counting via a Projected Model Counter -- 4.1 Basic MUS Counting Idea -- 4.2 W1 - the Base Wrapper and Its Reminder -- 4.3 W2 - the Intersection of MUSes -- 4.4 W3 - The Union of MUSes -- 4.5 W4 - Minimum MUS Cardinality -- 4.6 W5 - Maximum MUS Cardinality -- 4.7 W6 - Component Partitioning.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">4.8 W7 - Minimal Hitting Set Duality -- 4.9 W8 - Literal Negation Cover -- 4.10 W9 - Non-extendable Evidence Models -- 4.11 W10 - Enforced Evidence Models -- 4.12 Combining Wrappers and Their Remainders -- 5 Experimental Evaluation -- 5.1 Solved Benchmarks -- 5.2 Scalability W.r.t the MUS Count -- 5.3 Accuracy of Wrappers -- 6 Future Possible Applications of Wrappers and Remainders -- 7 Conclusion and Future Work -- References -- Sound Verification Procedures for Temporal Properties of Infinite-State Systems -- 1 Introduction -- 2 The Cervino Language -- 2.1 Sorts, Relations and Axioms -- 2.2 Events -- 2.3 Commands -- 3 Background on FOLTL -- 3.1 Syntax and Semantics of FOLTL -- 3.2 Bounded Domain Property -- 3.3 Semantics of Cervino -- 4 Basic Transformations -- 4.1 Transforming Equality -- 4.2 Restricted Skolemization -- 4.3 Instantiation -- 4.4 Addressing Transitive Closure and the Between Relation -- 4.5 Geneva Transformation -- 5 TEA: Transforming Existential Quantifiers -- 6 TFC: Transforming Frame Conditions -- 7 TTC: Transforming Reflexive-Transitive Closure -- 8 Evaluation -- 9 Related Work -- 10 Conclusion -- References -- Hardware and Model Checking -- Progress in Certifying Hardware Model Checking Results -- 1 Introduction -- 2 Circuits -- 3 Model Checking -- 4 Certification -- 5 Implementation -- 6 Experiments -- 7 Conclusion -- References -- Model-Checking Structured Context-Free Languages -- 1 Introduction -- 2 Operator Precedence Languages -- 2.1 Operator Precedence Omega-Languages -- 2.2 Modeling Programs with OPA -- 3 POTL: Syntax and Semantics -- 3.1 Expressiveness of POTL -- 4 Model Checking -- 4.1 Model Checking for Omega-Words -- 4.2 Complexity -- 5 Experimental Evaluation -- 6 Conclusions -- References -- Model Checking -Regular Properties with Decoupled Search -- 1 Introduction -- 2 Büchi Automata, Composition and Verification.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">3 The Decoupled State Space for Composed NBAs.</subfield></datafield><datafield tag="588" ind1=" " ind2=" "><subfield code="a">Description based on publisher supplied metadata and other sources.</subfield></datafield><datafield tag="590" ind1=" " ind2=" "><subfield code="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. </subfield></datafield><datafield tag="655" ind1=" " ind2="4"><subfield code="a">Electronic books.</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Leino, K. Rustan M.</subfield></datafield><datafield tag="776" ind1="0" ind2="8"><subfield code="i">Print version:</subfield><subfield code="a">Silva, Alexandra</subfield><subfield code="t">Computer Aided Verification</subfield><subfield code="d">Cham : Springer International Publishing AG,c2021</subfield><subfield code="z">9783030816872</subfield></datafield><datafield tag="797" ind1="2" ind2=" "><subfield code="a">ProQuest (Firm)</subfield></datafield><datafield tag="830" ind1=" " ind2="0"><subfield code="a">Lecture Notes in Computer Science Series</subfield></datafield><datafield tag="856" ind1="4" ind2="0"><subfield code="u">https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6679368</subfield><subfield code="z">Click to View</subfield></datafield></record></collection> |