Computer Aided Verification : : 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I.

• Superior document: Lecture Notes in Computer Science Series ; v.12759
• Author: Silva, Alexandra.
• TeilnehmendeR: Leino, K. Rustan M.
• 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
• Physical Description: 1 online resource (939 pages)

Table of 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.