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.