Computer Aided Verification : : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I.
Saved in:
Superior document: | Lecture Notes in Computer Science Series ; v.12759 |
---|---|
: | |
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 (939 pages) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
5006679367 |
---|---|
ctrlnum |
(MiAaPQ)5006679367 (Au-PeEL)EBL6679367 (OCoLC)1261896777 |
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 I. 1st ed. Cham : Springer International Publishing AG, 2021. ©2021. 1 online resource (939 pages) text txt rdacontent computer c rdamedia online resource cr rdacarrier Lecture Notes in Computer Science Series ; v.12759 Intro -- Preface -- Organization -- Contents - Part I -- Contents - Part II -- Invited Papers -- NNREPAIR: Constraint-Based Repair of Neural Network Classifiers -- 1 Introduction -- 2 Background -- 3 Example -- 4 Approach -- 4.1 Intermediate-Layer Repair -- 4.2 Last-Layer Repair -- 4.3 Combining Experts -- 5 Evaluation -- 5.1 Scenarios -- 5.2 Experiment Set-Up -- 5.3 Results -- 5.4 Discussion -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Balancing Automation and Control for Formal Verification of Microprocessors -- 1 Introduction -- 2 Our FV Tools -- 3 Challenges of Verifying a Single x86 instruction -- 3.1 Front-End and Microcode Verification -- 3.2 Verification of Execution Units -- 3.3 Regressions -- 4 FGL -- 4.1 Example -- 4.2 Extracting Boolean Variables -- 4.3 Composing Boolean Functions -- 5 Conclusion -- References -- Algebraic Program Analysis -- 1 Introduction -- 2 Regular Algebraic Program Analysis -- 2.1 Transition-Formula Interpretations -- 2.2 Weak Interpretations -- 3 Semantic Foundations -- 3.1 Semantic Equations -- 3.2 Abstract Interpretation -- 3.3 Discussion -- 4 Interprocedural Analysis -- 4.1 Motivation: Newtonian Program Analysis -- 4.2 Algebraic Program Analysis for Linear Equations -- 4.3 Discussion -- 5 Termination Analysis -- 5.1 Non-terminating State-Formula Interpretations -- 5.2 The Instantiation of the Recipe -- 6 Recap -- 7 Related Work -- 8 Open Problems -- References -- Programmable Program Synthesis -- 1 Introduction -- 1.1 A Synthesis Tale -- 1.2 Programmable Synthesis Frameworks -- 2 An Overview of Programmable Program Synthesis -- 2.1 Why Isn't Existing Work in Synthesis Programmable? -- 2.2 What Does a Programmable Synthesis Framework Look Like? -- 3 Programmable-Synthesis Specifications -- 3.1 Semantics-Guided Synthesis -- 3.2 Adding Quantitative Syntactic Objectives. 4 Programmable-Synthesis Solvers -- 4.1 General Solving Procedures for SemGuS Problems -- 4.2 Meta Algorithms for Solving SemGuS Problems -- 5 The Future of Programmable Synthesis and SemGuS -- 5.1 What Are We Working on Next? -- 5.2 What Can the Synthesis Community Do? -- References -- Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities -- 1 Introduction -- 2 State of the Art -- 2.1 Specifications -- 2.2 The Basics of Deductive Synthesis -- 2.3 Synthesis with Recursion and Auxiliary Functions -- 2.4 Implementation and Empirical Results -- 3 Proof Search -- 3.1 Pruning via Proof Strategies -- 3.2 Prioritization via a Cost Function -- 4 Completeness -- 4.1 Recursive Auxiliaries -- 4.2 Pure Reasoning -- 5 Quality of Synthesized Programs -- 5.1 Performance -- 5.2 Readability -- 6 Applications -- 6.1 Program Repair -- 6.2 Data Migration and Serialization -- 6.3 Fine-Grained Concurrency -- References -- AI Verification -- DNNV: A Framework for Deep Neural Network Verification -- 1 Introduction -- 2 Background -- 3 DNNV Overview -- 3.1 Input Formats -- 3.2 Network Simplification -- 3.3 Property Reduction -- 3.4 Input and Output Translation -- 4 Implementation -- 4.1 Supporting Reuse and Extension -- 4.2 Usage -- 5 Study -- 6 Conclusion -- References -- Robustness Verification of Quantum Classifiers -- 1 Introduction -- 2 Quantum Data and Computation Models -- 3 Quantum Classification Algorithms -- 3.1 Basic Definitions -- 3.2 An Illustrative Example -- 4 Robustness -- 5 Robust Bound -- 6 Robustness Verification Algorithms -- 7 Evaluation -- 7.1 Quantum Bits Classification -- 7.2 Quantum Phase Recognition -- 7.3 Cluster Excitation Detection -- 7.4 The Classification of MNIST -- 7.5 Robustness Verification -- 8 Conclusion -- References -- BDD4BNN: A BDD-Based Quantitative Analysis Framework for Binarized Neural Networks. 1 Introduction -- 2 Preliminaries -- 2.1 Binarized Neural Networks -- 2.2 Binary Decision Diagrams -- 3 BDD4BNN Design -- 3.1 BDD4BNN Overview -- 3.2 CC2BDD: Cardinality Constraints to BDDs -- 3.3 Region2BDD: Input Regions to BDDs -- 3.4 BNN2CC: BNNs to Cardinality Constraints -- 3.5 BDD Model Builder -- 4 Applications: Robustness Analysis and Interpretability -- 4.1 Robustness Analysis -- 4.2 Interpretability -- 5 Evaluation -- 5.1 Performance of BDD Encoding -- 5.2 Robustness Analysis -- 5.3 Interpretability -- 6 Related Work -- 7 Conclusion -- References -- Automated Safety Verification of Programs Invoking Neural Networks -- 1 Introduction -- 2 Overview -- 3 Approach -- 3.1 Neuro-Aware Program Analysis -- 3.2 Neural-Network Analysis -- 4 Experimental Evaluation -- 4.1 Benchmarks -- 4.2 Implementation -- 4.3 Setup -- 4.4 Results -- 5 Related Work -- 6 Conclusion -- References -- Scalable Polyhedral Verification of Recurrent Neural Networks -- 1 Introduction -- 2 Related Work -- 3 Background -- 3.1 Threat Model -- 3.2 Long Short-Term Memory (LSTM) -- 3.3 Speech Preprocessing -- 3.4 Verification Using DeepPoly Abstract Domain -- 4 Overview of Prover -- 5 Scalable Certification of LSTMs -- 5.1 Computing Polyhedral Abstractions of LSTM Operations -- 5.2 Abstraction Refinement via Optimization -- 6 Certification of Speech Preprocessing -- 7 Experimental Evaluation -- 7.1 Speech Classification -- 7.2 Image Classification -- 7.3 Motion Sensor Data Classification -- 8 Conclusion -- References -- Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning -- 1 Introduction -- 2 Problem Statement -- 3 Background: Neural Networks as Taylor Models -- 4 Taylor Model Preconditioning and Shrink Wrapping -- 4.1 Taylor Model Preconditioning -- 4.2 Shrink Wrapping -- 5 Implementation -- 6 Benchmarks -- 7 Experiments -- 8 Conclusion. References -- Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability -- 1 Introduction -- 2 Preliminaries and Problem Formulation -- 2.1 ImageStars -- 2.2 Range of a Specific Input in an ImageStar -- 2.3 Semantic Segmentation Networks and Reachability -- 2.4 Adversarial Attacks and Robustness -- 2.5 Robustness Verification Problem Formulation -- 3 Reachability of SSNs Using Relaxed ImageStars -- 3.1 Reachability of a Transposed (Dilated) Convolutional Layer -- 3.2 Relaxed Reachability of a ReLU Layer -- 3.3 Reachability of a Pixel-Classification Layer -- 4 Verification Algorithm -- 5 Evaluation -- 5.1 Robustness and Sensitivity of Different Network Architectures -- 5.2 Verification Performance -- 5.3 Reducing Verification Time with Relaxation -- 5.4 Conservativeness of Different Relaxation Heuristics -- 6 Related Work -- 7 Conclusion -- References -- PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier -- 1 Introduction -- 2 Problem Formulation -- 3 PEREGRiNN Overview -- 4 PEREGRiNN Enhancements -- 4.1 Sum-of-Slacks Penalty -- 4.2 Max-Slack Conditioning Priority -- 4.3 Layer-wise-Weighted Penalty -- 4.4 Initial Counterexample Search by Sampling -- 5 Experiments -- 5.1 Adversarial Robustness Verification Task -- 5.2 Ablation Experiments -- 5.3 Comparison with Other NN Verifiers -- 6 Discussion: Analogy to SAT Solvers -- 7 Conclusion -- References -- Concurrency and Blockchain -- Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models -- 1 Introduction -- 2 Implementation -- 2.1 Symbolic Execution for Sail -- 2.2 Checking a Litmus Test -- 2.3 Syntactic Dependency Analysis -- 2.4 Web Interface -- 3 System Litmus Tests -- 4 Results and Comparisons -- References -- Summing up Smart Transitions -- 1 Introduction -- 2 Preliminaries -- 3 Sum Logic (SL) -- 4 Decidability of SL. 4.1 A Decidable Fragment of SL -- 4.2 SL Undecidability -- 5 SL Encodings of Smart Transitions -- 5.1 SL Encoding Using Implicit Balances and Sums -- 5.2 Completeness Relative to a Translation Function -- 5.3 SL Encodings Using Explicit Balances and Sums -- 6 Experiments -- 7 Related Work -- 8 Conclusions -- References -- Stateless Model Checking Under a Reads-Value-From Equivalence -- 1 Introduction -- 1.1 Motivating Example -- 1.2 Our Contributions -- 2 Preliminaries -- 2.1 Concurrent Model -- 2.2 Partial Orders -- 3 Reads-Value-From Equivalence -- 4 Verifying Sequential Consistency -- 4.1 Algorithm for VSC -- 4.2 Practical Heuristics for VerifySC in SMC -- 5 Stateless Model Checking -- 6 Experiments -- 7 Conclusions -- References -- Gobra: Modular Specification and Verification of Go Programs -- 1 Introduction -- 2 Gobra in a Nutshell -- 2.1 Basics -- 2.2 Interfaces -- 2.3 Concurrency -- 3 Encoding -- 4 Implementation and Evaluation -- 5 Related Work and Conclusion -- References -- Delay-Bounded Scheduling Without Delay! -- 1 Introduction -- 2 Delay-Bounded Scheduling -- 2.1 Basic Computational Model -- 2.2 Free and Round-Robin Scheduling -- 2.3 Delay-Bounded Round-Robin Scheduling -- 3 Abstract Closure for Delay-Bounded Analysis -- 3.1 Respectful Actions -- 3.2 From Delay-Bounded to Delay-Unbounded Analysis -- 4 Efficient Delay-Unbounded Analysis -- 5 DrUBA with Unbounded-Domain Variables -- 5.1 The Fixed-Thread Case -- 5.2 The Unbounded-Thread Case -- 6 Evaluation -- 6.1 Results -- 6.2 Unbounded-Thread Experiments -- 7 Discussion of Related Work -- 8 Conclusion -- References -- Checking Data-Race Freedom of GPU Kernels, Compositionally -- 1 Introduction -- 2 Overview -- 2.1 Challenges of GPU Programming -- 2.2 Memory Access Protocols by Example -- 3 Access Memory Protocols -- 4 DRF-Preserving Transformations of Protocols. 4.1 Aligning Protocols. 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 9783030816841 ProQuest (Firm) Lecture Notes in Computer Science Series https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6679367 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 I. Lecture Notes in Computer Science Series ; Intro -- Preface -- Organization -- Contents - Part I -- Contents - Part II -- Invited Papers -- NNREPAIR: Constraint-Based Repair of Neural Network Classifiers -- 1 Introduction -- 2 Background -- 3 Example -- 4 Approach -- 4.1 Intermediate-Layer Repair -- 4.2 Last-Layer Repair -- 4.3 Combining Experts -- 5 Evaluation -- 5.1 Scenarios -- 5.2 Experiment Set-Up -- 5.3 Results -- 5.4 Discussion -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Balancing Automation and Control for Formal Verification of Microprocessors -- 1 Introduction -- 2 Our FV Tools -- 3 Challenges of Verifying a Single x86 instruction -- 3.1 Front-End and Microcode Verification -- 3.2 Verification of Execution Units -- 3.3 Regressions -- 4 FGL -- 4.1 Example -- 4.2 Extracting Boolean Variables -- 4.3 Composing Boolean Functions -- 5 Conclusion -- References -- Algebraic Program Analysis -- 1 Introduction -- 2 Regular Algebraic Program Analysis -- 2.1 Transition-Formula Interpretations -- 2.2 Weak Interpretations -- 3 Semantic Foundations -- 3.1 Semantic Equations -- 3.2 Abstract Interpretation -- 3.3 Discussion -- 4 Interprocedural Analysis -- 4.1 Motivation: Newtonian Program Analysis -- 4.2 Algebraic Program Analysis for Linear Equations -- 4.3 Discussion -- 5 Termination Analysis -- 5.1 Non-terminating State-Formula Interpretations -- 5.2 The Instantiation of the Recipe -- 6 Recap -- 7 Related Work -- 8 Open Problems -- References -- Programmable Program Synthesis -- 1 Introduction -- 1.1 A Synthesis Tale -- 1.2 Programmable Synthesis Frameworks -- 2 An Overview of Programmable Program Synthesis -- 2.1 Why Isn't Existing Work in Synthesis Programmable? -- 2.2 What Does a Programmable Synthesis Framework Look Like? -- 3 Programmable-Synthesis Specifications -- 3.1 Semantics-Guided Synthesis -- 3.2 Adding Quantitative Syntactic Objectives. 4 Programmable-Synthesis Solvers -- 4.1 General Solving Procedures for SemGuS Problems -- 4.2 Meta Algorithms for Solving SemGuS Problems -- 5 The Future of Programmable Synthesis and SemGuS -- 5.1 What Are We Working on Next? -- 5.2 What Can the Synthesis Community Do? -- References -- Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities -- 1 Introduction -- 2 State of the Art -- 2.1 Specifications -- 2.2 The Basics of Deductive Synthesis -- 2.3 Synthesis with Recursion and Auxiliary Functions -- 2.4 Implementation and Empirical Results -- 3 Proof Search -- 3.1 Pruning via Proof Strategies -- 3.2 Prioritization via a Cost Function -- 4 Completeness -- 4.1 Recursive Auxiliaries -- 4.2 Pure Reasoning -- 5 Quality of Synthesized Programs -- 5.1 Performance -- 5.2 Readability -- 6 Applications -- 6.1 Program Repair -- 6.2 Data Migration and Serialization -- 6.3 Fine-Grained Concurrency -- References -- AI Verification -- DNNV: A Framework for Deep Neural Network Verification -- 1 Introduction -- 2 Background -- 3 DNNV Overview -- 3.1 Input Formats -- 3.2 Network Simplification -- 3.3 Property Reduction -- 3.4 Input and Output Translation -- 4 Implementation -- 4.1 Supporting Reuse and Extension -- 4.2 Usage -- 5 Study -- 6 Conclusion -- References -- Robustness Verification of Quantum Classifiers -- 1 Introduction -- 2 Quantum Data and Computation Models -- 3 Quantum Classification Algorithms -- 3.1 Basic Definitions -- 3.2 An Illustrative Example -- 4 Robustness -- 5 Robust Bound -- 6 Robustness Verification Algorithms -- 7 Evaluation -- 7.1 Quantum Bits Classification -- 7.2 Quantum Phase Recognition -- 7.3 Cluster Excitation Detection -- 7.4 The Classification of MNIST -- 7.5 Robustness Verification -- 8 Conclusion -- References -- BDD4BNN: A BDD-Based Quantitative Analysis Framework for Binarized Neural Networks. 1 Introduction -- 2 Preliminaries -- 2.1 Binarized Neural Networks -- 2.2 Binary Decision Diagrams -- 3 BDD4BNN Design -- 3.1 BDD4BNN Overview -- 3.2 CC2BDD: Cardinality Constraints to BDDs -- 3.3 Region2BDD: Input Regions to BDDs -- 3.4 BNN2CC: BNNs to Cardinality Constraints -- 3.5 BDD Model Builder -- 4 Applications: Robustness Analysis and Interpretability -- 4.1 Robustness Analysis -- 4.2 Interpretability -- 5 Evaluation -- 5.1 Performance of BDD Encoding -- 5.2 Robustness Analysis -- 5.3 Interpretability -- 6 Related Work -- 7 Conclusion -- References -- Automated Safety Verification of Programs Invoking Neural Networks -- 1 Introduction -- 2 Overview -- 3 Approach -- 3.1 Neuro-Aware Program Analysis -- 3.2 Neural-Network Analysis -- 4 Experimental Evaluation -- 4.1 Benchmarks -- 4.2 Implementation -- 4.3 Setup -- 4.4 Results -- 5 Related Work -- 6 Conclusion -- References -- Scalable Polyhedral Verification of Recurrent Neural Networks -- 1 Introduction -- 2 Related Work -- 3 Background -- 3.1 Threat Model -- 3.2 Long Short-Term Memory (LSTM) -- 3.3 Speech Preprocessing -- 3.4 Verification Using DeepPoly Abstract Domain -- 4 Overview of Prover -- 5 Scalable Certification of LSTMs -- 5.1 Computing Polyhedral Abstractions of LSTM Operations -- 5.2 Abstraction Refinement via Optimization -- 6 Certification of Speech Preprocessing -- 7 Experimental Evaluation -- 7.1 Speech Classification -- 7.2 Image Classification -- 7.3 Motion Sensor Data Classification -- 8 Conclusion -- References -- Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning -- 1 Introduction -- 2 Problem Statement -- 3 Background: Neural Networks as Taylor Models -- 4 Taylor Model Preconditioning and Shrink Wrapping -- 4.1 Taylor Model Preconditioning -- 4.2 Shrink Wrapping -- 5 Implementation -- 6 Benchmarks -- 7 Experiments -- 8 Conclusion. References -- Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability -- 1 Introduction -- 2 Preliminaries and Problem Formulation -- 2.1 ImageStars -- 2.2 Range of a Specific Input in an ImageStar -- 2.3 Semantic Segmentation Networks and Reachability -- 2.4 Adversarial Attacks and Robustness -- 2.5 Robustness Verification Problem Formulation -- 3 Reachability of SSNs Using Relaxed ImageStars -- 3.1 Reachability of a Transposed (Dilated) Convolutional Layer -- 3.2 Relaxed Reachability of a ReLU Layer -- 3.3 Reachability of a Pixel-Classification Layer -- 4 Verification Algorithm -- 5 Evaluation -- 5.1 Robustness and Sensitivity of Different Network Architectures -- 5.2 Verification Performance -- 5.3 Reducing Verification Time with Relaxation -- 5.4 Conservativeness of Different Relaxation Heuristics -- 6 Related Work -- 7 Conclusion -- References -- PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier -- 1 Introduction -- 2 Problem Formulation -- 3 PEREGRiNN Overview -- 4 PEREGRiNN Enhancements -- 4.1 Sum-of-Slacks Penalty -- 4.2 Max-Slack Conditioning Priority -- 4.3 Layer-wise-Weighted Penalty -- 4.4 Initial Counterexample Search by Sampling -- 5 Experiments -- 5.1 Adversarial Robustness Verification Task -- 5.2 Ablation Experiments -- 5.3 Comparison with Other NN Verifiers -- 6 Discussion: Analogy to SAT Solvers -- 7 Conclusion -- References -- Concurrency and Blockchain -- Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models -- 1 Introduction -- 2 Implementation -- 2.1 Symbolic Execution for Sail -- 2.2 Checking a Litmus Test -- 2.3 Syntactic Dependency Analysis -- 2.4 Web Interface -- 3 System Litmus Tests -- 4 Results and Comparisons -- References -- Summing up Smart Transitions -- 1 Introduction -- 2 Preliminaries -- 3 Sum Logic (SL) -- 4 Decidability of SL. 4.1 A Decidable Fragment of SL -- 4.2 SL Undecidability -- 5 SL Encodings of Smart Transitions -- 5.1 SL Encoding Using Implicit Balances and Sums -- 5.2 Completeness Relative to a Translation Function -- 5.3 SL Encodings Using Explicit Balances and Sums -- 6 Experiments -- 7 Related Work -- 8 Conclusions -- References -- Stateless Model Checking Under a Reads-Value-From Equivalence -- 1 Introduction -- 1.1 Motivating Example -- 1.2 Our Contributions -- 2 Preliminaries -- 2.1 Concurrent Model -- 2.2 Partial Orders -- 3 Reads-Value-From Equivalence -- 4 Verifying Sequential Consistency -- 4.1 Algorithm for VSC -- 4.2 Practical Heuristics for VerifySC in SMC -- 5 Stateless Model Checking -- 6 Experiments -- 7 Conclusions -- References -- Gobra: Modular Specification and Verification of Go Programs -- 1 Introduction -- 2 Gobra in a Nutshell -- 2.1 Basics -- 2.2 Interfaces -- 2.3 Concurrency -- 3 Encoding -- 4 Implementation and Evaluation -- 5 Related Work and Conclusion -- References -- Delay-Bounded Scheduling Without Delay! -- 1 Introduction -- 2 Delay-Bounded Scheduling -- 2.1 Basic Computational Model -- 2.2 Free and Round-Robin Scheduling -- 2.3 Delay-Bounded Round-Robin Scheduling -- 3 Abstract Closure for Delay-Bounded Analysis -- 3.1 Respectful Actions -- 3.2 From Delay-Bounded to Delay-Unbounded Analysis -- 4 Efficient Delay-Unbounded Analysis -- 5 DrUBA with Unbounded-Domain Variables -- 5.1 The Fixed-Thread Case -- 5.2 The Unbounded-Thread Case -- 6 Evaluation -- 6.1 Results -- 6.2 Unbounded-Thread Experiments -- 7 Discussion of Related Work -- 8 Conclusion -- References -- Checking Data-Race Freedom of GPU Kernels, Compositionally -- 1 Introduction -- 2 Overview -- 2.1 Challenges of GPU Programming -- 2.2 Memory Access Protocols by Example -- 3 Access Memory Protocols -- 4 DRF-Preserving Transformations of Protocols. 4.1 Aligning Protocols. |
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 I. |
title_sub |
33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I. |
title_full |
Computer Aided Verification : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I. |
title_fullStr |
Computer Aided Verification : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I. |
title_full_unstemmed |
Computer Aided Verification : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I. |
title_auth |
Computer Aided Verification : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I. |
title_new |
Computer Aided Verification : |
title_sort |
computer aided verification : 33rd international conference, cav 2021, virtual event, july 20-23, 2021, proceedings, part i. |
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 (939 pages) |
edition |
1st ed. |
contents |
Intro -- Preface -- Organization -- Contents - Part I -- Contents - Part II -- Invited Papers -- NNREPAIR: Constraint-Based Repair of Neural Network Classifiers -- 1 Introduction -- 2 Background -- 3 Example -- 4 Approach -- 4.1 Intermediate-Layer Repair -- 4.2 Last-Layer Repair -- 4.3 Combining Experts -- 5 Evaluation -- 5.1 Scenarios -- 5.2 Experiment Set-Up -- 5.3 Results -- 5.4 Discussion -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Balancing Automation and Control for Formal Verification of Microprocessors -- 1 Introduction -- 2 Our FV Tools -- 3 Challenges of Verifying a Single x86 instruction -- 3.1 Front-End and Microcode Verification -- 3.2 Verification of Execution Units -- 3.3 Regressions -- 4 FGL -- 4.1 Example -- 4.2 Extracting Boolean Variables -- 4.3 Composing Boolean Functions -- 5 Conclusion -- References -- Algebraic Program Analysis -- 1 Introduction -- 2 Regular Algebraic Program Analysis -- 2.1 Transition-Formula Interpretations -- 2.2 Weak Interpretations -- 3 Semantic Foundations -- 3.1 Semantic Equations -- 3.2 Abstract Interpretation -- 3.3 Discussion -- 4 Interprocedural Analysis -- 4.1 Motivation: Newtonian Program Analysis -- 4.2 Algebraic Program Analysis for Linear Equations -- 4.3 Discussion -- 5 Termination Analysis -- 5.1 Non-terminating State-Formula Interpretations -- 5.2 The Instantiation of the Recipe -- 6 Recap -- 7 Related Work -- 8 Open Problems -- References -- Programmable Program Synthesis -- 1 Introduction -- 1.1 A Synthesis Tale -- 1.2 Programmable Synthesis Frameworks -- 2 An Overview of Programmable Program Synthesis -- 2.1 Why Isn't Existing Work in Synthesis Programmable? -- 2.2 What Does a Programmable Synthesis Framework Look Like? -- 3 Programmable-Synthesis Specifications -- 3.1 Semantics-Guided Synthesis -- 3.2 Adding Quantitative Syntactic Objectives. 4 Programmable-Synthesis Solvers -- 4.1 General Solving Procedures for SemGuS Problems -- 4.2 Meta Algorithms for Solving SemGuS Problems -- 5 The Future of Programmable Synthesis and SemGuS -- 5.1 What Are We Working on Next? -- 5.2 What Can the Synthesis Community Do? -- References -- Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities -- 1 Introduction -- 2 State of the Art -- 2.1 Specifications -- 2.2 The Basics of Deductive Synthesis -- 2.3 Synthesis with Recursion and Auxiliary Functions -- 2.4 Implementation and Empirical Results -- 3 Proof Search -- 3.1 Pruning via Proof Strategies -- 3.2 Prioritization via a Cost Function -- 4 Completeness -- 4.1 Recursive Auxiliaries -- 4.2 Pure Reasoning -- 5 Quality of Synthesized Programs -- 5.1 Performance -- 5.2 Readability -- 6 Applications -- 6.1 Program Repair -- 6.2 Data Migration and Serialization -- 6.3 Fine-Grained Concurrency -- References -- AI Verification -- DNNV: A Framework for Deep Neural Network Verification -- 1 Introduction -- 2 Background -- 3 DNNV Overview -- 3.1 Input Formats -- 3.2 Network Simplification -- 3.3 Property Reduction -- 3.4 Input and Output Translation -- 4 Implementation -- 4.1 Supporting Reuse and Extension -- 4.2 Usage -- 5 Study -- 6 Conclusion -- References -- Robustness Verification of Quantum Classifiers -- 1 Introduction -- 2 Quantum Data and Computation Models -- 3 Quantum Classification Algorithms -- 3.1 Basic Definitions -- 3.2 An Illustrative Example -- 4 Robustness -- 5 Robust Bound -- 6 Robustness Verification Algorithms -- 7 Evaluation -- 7.1 Quantum Bits Classification -- 7.2 Quantum Phase Recognition -- 7.3 Cluster Excitation Detection -- 7.4 The Classification of MNIST -- 7.5 Robustness Verification -- 8 Conclusion -- References -- BDD4BNN: A BDD-Based Quantitative Analysis Framework for Binarized Neural Networks. 1 Introduction -- 2 Preliminaries -- 2.1 Binarized Neural Networks -- 2.2 Binary Decision Diagrams -- 3 BDD4BNN Design -- 3.1 BDD4BNN Overview -- 3.2 CC2BDD: Cardinality Constraints to BDDs -- 3.3 Region2BDD: Input Regions to BDDs -- 3.4 BNN2CC: BNNs to Cardinality Constraints -- 3.5 BDD Model Builder -- 4 Applications: Robustness Analysis and Interpretability -- 4.1 Robustness Analysis -- 4.2 Interpretability -- 5 Evaluation -- 5.1 Performance of BDD Encoding -- 5.2 Robustness Analysis -- 5.3 Interpretability -- 6 Related Work -- 7 Conclusion -- References -- Automated Safety Verification of Programs Invoking Neural Networks -- 1 Introduction -- 2 Overview -- 3 Approach -- 3.1 Neuro-Aware Program Analysis -- 3.2 Neural-Network Analysis -- 4 Experimental Evaluation -- 4.1 Benchmarks -- 4.2 Implementation -- 4.3 Setup -- 4.4 Results -- 5 Related Work -- 6 Conclusion -- References -- Scalable Polyhedral Verification of Recurrent Neural Networks -- 1 Introduction -- 2 Related Work -- 3 Background -- 3.1 Threat Model -- 3.2 Long Short-Term Memory (LSTM) -- 3.3 Speech Preprocessing -- 3.4 Verification Using DeepPoly Abstract Domain -- 4 Overview of Prover -- 5 Scalable Certification of LSTMs -- 5.1 Computing Polyhedral Abstractions of LSTM Operations -- 5.2 Abstraction Refinement via Optimization -- 6 Certification of Speech Preprocessing -- 7 Experimental Evaluation -- 7.1 Speech Classification -- 7.2 Image Classification -- 7.3 Motion Sensor Data Classification -- 8 Conclusion -- References -- Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning -- 1 Introduction -- 2 Problem Statement -- 3 Background: Neural Networks as Taylor Models -- 4 Taylor Model Preconditioning and Shrink Wrapping -- 4.1 Taylor Model Preconditioning -- 4.2 Shrink Wrapping -- 5 Implementation -- 6 Benchmarks -- 7 Experiments -- 8 Conclusion. References -- Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability -- 1 Introduction -- 2 Preliminaries and Problem Formulation -- 2.1 ImageStars -- 2.2 Range of a Specific Input in an ImageStar -- 2.3 Semantic Segmentation Networks and Reachability -- 2.4 Adversarial Attacks and Robustness -- 2.5 Robustness Verification Problem Formulation -- 3 Reachability of SSNs Using Relaxed ImageStars -- 3.1 Reachability of a Transposed (Dilated) Convolutional Layer -- 3.2 Relaxed Reachability of a ReLU Layer -- 3.3 Reachability of a Pixel-Classification Layer -- 4 Verification Algorithm -- 5 Evaluation -- 5.1 Robustness and Sensitivity of Different Network Architectures -- 5.2 Verification Performance -- 5.3 Reducing Verification Time with Relaxation -- 5.4 Conservativeness of Different Relaxation Heuristics -- 6 Related Work -- 7 Conclusion -- References -- PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier -- 1 Introduction -- 2 Problem Formulation -- 3 PEREGRiNN Overview -- 4 PEREGRiNN Enhancements -- 4.1 Sum-of-Slacks Penalty -- 4.2 Max-Slack Conditioning Priority -- 4.3 Layer-wise-Weighted Penalty -- 4.4 Initial Counterexample Search by Sampling -- 5 Experiments -- 5.1 Adversarial Robustness Verification Task -- 5.2 Ablation Experiments -- 5.3 Comparison with Other NN Verifiers -- 6 Discussion: Analogy to SAT Solvers -- 7 Conclusion -- References -- Concurrency and Blockchain -- Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models -- 1 Introduction -- 2 Implementation -- 2.1 Symbolic Execution for Sail -- 2.2 Checking a Litmus Test -- 2.3 Syntactic Dependency Analysis -- 2.4 Web Interface -- 3 System Litmus Tests -- 4 Results and Comparisons -- References -- Summing up Smart Transitions -- 1 Introduction -- 2 Preliminaries -- 3 Sum Logic (SL) -- 4 Decidability of SL. 4.1 A Decidable Fragment of SL -- 4.2 SL Undecidability -- 5 SL Encodings of Smart Transitions -- 5.1 SL Encoding Using Implicit Balances and Sums -- 5.2 Completeness Relative to a Translation Function -- 5.3 SL Encodings Using Explicit Balances and Sums -- 6 Experiments -- 7 Related Work -- 8 Conclusions -- References -- Stateless Model Checking Under a Reads-Value-From Equivalence -- 1 Introduction -- 1.1 Motivating Example -- 1.2 Our Contributions -- 2 Preliminaries -- 2.1 Concurrent Model -- 2.2 Partial Orders -- 3 Reads-Value-From Equivalence -- 4 Verifying Sequential Consistency -- 4.1 Algorithm for VSC -- 4.2 Practical Heuristics for VerifySC in SMC -- 5 Stateless Model Checking -- 6 Experiments -- 7 Conclusions -- References -- Gobra: Modular Specification and Verification of Go Programs -- 1 Introduction -- 2 Gobra in a Nutshell -- 2.1 Basics -- 2.2 Interfaces -- 2.3 Concurrency -- 3 Encoding -- 4 Implementation and Evaluation -- 5 Related Work and Conclusion -- References -- Delay-Bounded Scheduling Without Delay! -- 1 Introduction -- 2 Delay-Bounded Scheduling -- 2.1 Basic Computational Model -- 2.2 Free and Round-Robin Scheduling -- 2.3 Delay-Bounded Round-Robin Scheduling -- 3 Abstract Closure for Delay-Bounded Analysis -- 3.1 Respectful Actions -- 3.2 From Delay-Bounded to Delay-Unbounded Analysis -- 4 Efficient Delay-Unbounded Analysis -- 5 DrUBA with Unbounded-Domain Variables -- 5.1 The Fixed-Thread Case -- 5.2 The Unbounded-Thread Case -- 6 Evaluation -- 6.1 Results -- 6.2 Unbounded-Thread Experiments -- 7 Discussion of Related Work -- 8 Conclusion -- References -- Checking Data-Race Freedom of GPU Kernels, Compositionally -- 1 Introduction -- 2 Overview -- 2.1 Challenges of GPU Programming -- 2.2 Memory Access Protocols by Example -- 3 Access Memory Protocols -- 4 DRF-Preserving Transformations of Protocols. 4.1 Aligning Protocols. |
isbn |
9783030816858 9783030816841 |
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=6679367 |
illustrated |
Not Illustrated |
oclc_num |
1261896777 |
work_keys_str_mv |
AT silvaalexandra computeraidedverification33rdinternationalconferencecav2021virtualeventjuly20232021proceedingsparti AT leinokrustanm computeraidedverification33rdinternationalconferencecav2021virtualeventjuly20232021proceedingsparti |
status_str |
n |
ids_txt_mv |
(MiAaPQ)5006679367 (Au-PeEL)EBL6679367 (OCoLC)1261896777 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Lecture Notes in Computer Science Series ; v.12759 |
is_hierarchy_title |
Computer Aided Verification : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I. |
container_title |
Lecture Notes in Computer Science Series ; v.12759 |
author2_original_writing_str_mv |
noLinkedField |
marc_error |
Info : MARC8 translation shorter than ISO-8859-1, choosing MARC8. --- [ 856 : z ] |
_version_ |
1792331059899138048 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>11153nam a22004693i 4500</leader><controlfield tag="001">5006679367</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">9783030816858</subfield><subfield code="q">(electronic bk.)</subfield></datafield><datafield tag="020" ind1=" " ind2=" "><subfield code="z">9783030816841</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(MiAaPQ)5006679367</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(Au-PeEL)EBL6679367</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(OCoLC)1261896777</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 I.</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 (939 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.12759</subfield></datafield><datafield tag="505" ind1="0" ind2=" "><subfield code="a">Intro -- Preface -- Organization -- Contents - Part I -- Contents - Part II -- Invited Papers -- NNREPAIR: Constraint-Based Repair of Neural Network Classifiers -- 1 Introduction -- 2 Background -- 3 Example -- 4 Approach -- 4.1 Intermediate-Layer Repair -- 4.2 Last-Layer Repair -- 4.3 Combining Experts -- 5 Evaluation -- 5.1 Scenarios -- 5.2 Experiment Set-Up -- 5.3 Results -- 5.4 Discussion -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Balancing Automation and Control for Formal Verification of Microprocessors -- 1 Introduction -- 2 Our FV Tools -- 3 Challenges of Verifying a Single x86 instruction -- 3.1 Front-End and Microcode Verification -- 3.2 Verification of Execution Units -- 3.3 Regressions -- 4 FGL -- 4.1 Example -- 4.2 Extracting Boolean Variables -- 4.3 Composing Boolean Functions -- 5 Conclusion -- References -- Algebraic Program Analysis -- 1 Introduction -- 2 Regular Algebraic Program Analysis -- 2.1 Transition-Formula Interpretations -- 2.2 Weak Interpretations -- 3 Semantic Foundations -- 3.1 Semantic Equations -- 3.2 Abstract Interpretation -- 3.3 Discussion -- 4 Interprocedural Analysis -- 4.1 Motivation: Newtonian Program Analysis -- 4.2 Algebraic Program Analysis for Linear Equations -- 4.3 Discussion -- 5 Termination Analysis -- 5.1 Non-terminating State-Formula Interpretations -- 5.2 The Instantiation of the Recipe -- 6 Recap -- 7 Related Work -- 8 Open Problems -- References -- Programmable Program Synthesis -- 1 Introduction -- 1.1 A Synthesis Tale -- 1.2 Programmable Synthesis Frameworks -- 2 An Overview of Programmable Program Synthesis -- 2.1 Why Isn't Existing Work in Synthesis Programmable? -- 2.2 What Does a Programmable Synthesis Framework Look Like? -- 3 Programmable-Synthesis Specifications -- 3.1 Semantics-Guided Synthesis -- 3.2 Adding Quantitative Syntactic Objectives.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">4 Programmable-Synthesis Solvers -- 4.1 General Solving Procedures for SemGuS Problems -- 4.2 Meta Algorithms for Solving SemGuS Problems -- 5 The Future of Programmable Synthesis and SemGuS -- 5.1 What Are We Working on Next? -- 5.2 What Can the Synthesis Community Do? -- References -- Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities -- 1 Introduction -- 2 State of the Art -- 2.1 Specifications -- 2.2 The Basics of Deductive Synthesis -- 2.3 Synthesis with Recursion and Auxiliary Functions -- 2.4 Implementation and Empirical Results -- 3 Proof Search -- 3.1 Pruning via Proof Strategies -- 3.2 Prioritization via a Cost Function -- 4 Completeness -- 4.1 Recursive Auxiliaries -- 4.2 Pure Reasoning -- 5 Quality of Synthesized Programs -- 5.1 Performance -- 5.2 Readability -- 6 Applications -- 6.1 Program Repair -- 6.2 Data Migration and Serialization -- 6.3 Fine-Grained Concurrency -- References -- AI Verification -- DNNV: A Framework for Deep Neural Network Verification -- 1 Introduction -- 2 Background -- 3 DNNV Overview -- 3.1 Input Formats -- 3.2 Network Simplification -- 3.3 Property Reduction -- 3.4 Input and Output Translation -- 4 Implementation -- 4.1 Supporting Reuse and Extension -- 4.2 Usage -- 5 Study -- 6 Conclusion -- References -- Robustness Verification of Quantum Classifiers -- 1 Introduction -- 2 Quantum Data and Computation Models -- 3 Quantum Classification Algorithms -- 3.1 Basic Definitions -- 3.2 An Illustrative Example -- 4 Robustness -- 5 Robust Bound -- 6 Robustness Verification Algorithms -- 7 Evaluation -- 7.1 Quantum Bits Classification -- 7.2 Quantum Phase Recognition -- 7.3 Cluster Excitation Detection -- 7.4 The Classification of MNIST -- 7.5 Robustness Verification -- 8 Conclusion -- References -- BDD4BNN: A BDD-Based Quantitative Analysis Framework for Binarized Neural Networks.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">1 Introduction -- 2 Preliminaries -- 2.1 Binarized Neural Networks -- 2.2 Binary Decision Diagrams -- 3 BDD4BNN Design -- 3.1 BDD4BNN Overview -- 3.2 CC2BDD: Cardinality Constraints to BDDs -- 3.3 Region2BDD: Input Regions to BDDs -- 3.4 BNN2CC: BNNs to Cardinality Constraints -- 3.5 BDD Model Builder -- 4 Applications: Robustness Analysis and Interpretability -- 4.1 Robustness Analysis -- 4.2 Interpretability -- 5 Evaluation -- 5.1 Performance of BDD Encoding -- 5.2 Robustness Analysis -- 5.3 Interpretability -- 6 Related Work -- 7 Conclusion -- References -- Automated Safety Verification of Programs Invoking Neural Networks -- 1 Introduction -- 2 Overview -- 3 Approach -- 3.1 Neuro-Aware Program Analysis -- 3.2 Neural-Network Analysis -- 4 Experimental Evaluation -- 4.1 Benchmarks -- 4.2 Implementation -- 4.3 Setup -- 4.4 Results -- 5 Related Work -- 6 Conclusion -- References -- Scalable Polyhedral Verification of Recurrent Neural Networks -- 1 Introduction -- 2 Related Work -- 3 Background -- 3.1 Threat Model -- 3.2 Long Short-Term Memory (LSTM) -- 3.3 Speech Preprocessing -- 3.4 Verification Using DeepPoly Abstract Domain -- 4 Overview of Prover -- 5 Scalable Certification of LSTMs -- 5.1 Computing Polyhedral Abstractions of LSTM Operations -- 5.2 Abstraction Refinement via Optimization -- 6 Certification of Speech Preprocessing -- 7 Experimental Evaluation -- 7.1 Speech Classification -- 7.2 Image Classification -- 7.3 Motion Sensor Data Classification -- 8 Conclusion -- References -- Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning -- 1 Introduction -- 2 Problem Statement -- 3 Background: Neural Networks as Taylor Models -- 4 Taylor Model Preconditioning and Shrink Wrapping -- 4.1 Taylor Model Preconditioning -- 4.2 Shrink Wrapping -- 5 Implementation -- 6 Benchmarks -- 7 Experiments -- 8 Conclusion.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">References -- Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability -- 1 Introduction -- 2 Preliminaries and Problem Formulation -- 2.1 ImageStars -- 2.2 Range of a Specific Input in an ImageStar -- 2.3 Semantic Segmentation Networks and Reachability -- 2.4 Adversarial Attacks and Robustness -- 2.5 Robustness Verification Problem Formulation -- 3 Reachability of SSNs Using Relaxed ImageStars -- 3.1 Reachability of a Transposed (Dilated) Convolutional Layer -- 3.2 Relaxed Reachability of a ReLU Layer -- 3.3 Reachability of a Pixel-Classification Layer -- 4 Verification Algorithm -- 5 Evaluation -- 5.1 Robustness and Sensitivity of Different Network Architectures -- 5.2 Verification Performance -- 5.3 Reducing Verification Time with Relaxation -- 5.4 Conservativeness of Different Relaxation Heuristics -- 6 Related Work -- 7 Conclusion -- References -- PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier -- 1 Introduction -- 2 Problem Formulation -- 3 PEREGRiNN Overview -- 4 PEREGRiNN Enhancements -- 4.1 Sum-of-Slacks Penalty -- 4.2 Max-Slack Conditioning Priority -- 4.3 Layer-wise-Weighted Penalty -- 4.4 Initial Counterexample Search by Sampling -- 5 Experiments -- 5.1 Adversarial Robustness Verification Task -- 5.2 Ablation Experiments -- 5.3 Comparison with Other NN Verifiers -- 6 Discussion: Analogy to SAT Solvers -- 7 Conclusion -- References -- Concurrency and Blockchain -- Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models -- 1 Introduction -- 2 Implementation -- 2.1 Symbolic Execution for Sail -- 2.2 Checking a Litmus Test -- 2.3 Syntactic Dependency Analysis -- 2.4 Web Interface -- 3 System Litmus Tests -- 4 Results and Comparisons -- References -- Summing up Smart Transitions -- 1 Introduction -- 2 Preliminaries -- 3 Sum Logic (SL) -- 4 Decidability of SL.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">4.1 A Decidable Fragment of SL -- 4.2 SL Undecidability -- 5 SL Encodings of Smart Transitions -- 5.1 SL Encoding Using Implicit Balances and Sums -- 5.2 Completeness Relative to a Translation Function -- 5.3 SL Encodings Using Explicit Balances and Sums -- 6 Experiments -- 7 Related Work -- 8 Conclusions -- References -- Stateless Model Checking Under a Reads-Value-From Equivalence -- 1 Introduction -- 1.1 Motivating Example -- 1.2 Our Contributions -- 2 Preliminaries -- 2.1 Concurrent Model -- 2.2 Partial Orders -- 3 Reads-Value-From Equivalence -- 4 Verifying Sequential Consistency -- 4.1 Algorithm for VSC -- 4.2 Practical Heuristics for VerifySC in SMC -- 5 Stateless Model Checking -- 6 Experiments -- 7 Conclusions -- References -- Gobra: Modular Specification and Verification of Go Programs -- 1 Introduction -- 2 Gobra in a Nutshell -- 2.1 Basics -- 2.2 Interfaces -- 2.3 Concurrency -- 3 Encoding -- 4 Implementation and Evaluation -- 5 Related Work and Conclusion -- References -- Delay-Bounded Scheduling Without Delay! -- 1 Introduction -- 2 Delay-Bounded Scheduling -- 2.1 Basic Computational Model -- 2.2 Free and Round-Robin Scheduling -- 2.3 Delay-Bounded Round-Robin Scheduling -- 3 Abstract Closure for Delay-Bounded Analysis -- 3.1 Respectful Actions -- 3.2 From Delay-Bounded to Delay-Unbounded Analysis -- 4 Efficient Delay-Unbounded Analysis -- 5 DrUBA with Unbounded-Domain Variables -- 5.1 The Fixed-Thread Case -- 5.2 The Unbounded-Thread Case -- 6 Evaluation -- 6.1 Results -- 6.2 Unbounded-Thread Experiments -- 7 Discussion of Related Work -- 8 Conclusion -- References -- Checking Data-Race Freedom of GPU Kernels, Compositionally -- 1 Introduction -- 2 Overview -- 2.1 Challenges of GPU Programming -- 2.2 Memory Access Protocols by Example -- 3 Access Memory Protocols -- 4 DRF-Preserving Transformations of Protocols.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">4.1 Aligning Protocols.</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">9783030816841</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=6679367</subfield><subfield code="z">Click to View</subfield></datafield></record></collection> |