Computer Aided Verification. 33rd International Conference, CAV 2021 Virtual Event, July 20–23, 2021 Proceedings

Description

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 4.2 Splitting Protocols into Symbolic Traces 5 Implementation 6 Experimental Evaluation 7 Related Work 8 Conclusion References GENMC: A Model Checker for Weak Memory Models 1 Introduction 2 Memory Model Requirements 3 Tool Architecture 4 Supporting New Memory Models 4.1 Supporting the Linux Kernel Memory Model (LKMM) 5 Supporting New Languages and Libraries 6 Error Detection and Reporting 7 Other Performance Enhancements to GenMC 8 Conclusion References Hybrid and Cyber-Physical Systems Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming 1 Introduction 2 A Bird's-Eye Perspective 3 Mathematical Foundations 4 Invariant Barrier-Certificate Condition as BMIs 4.1 Invariant Barrier-Certificate Condition 4.2 Encoding as BMI Optimizations 5 Solving BMI Optimizations via DCP 5.1 Difference-of-Convex Decomposition 5.2 Reduction to LMIs 5.3 Finding the Initial Solution 6 Incorporating in a Branch-and-Bound Framework 7 Experimental Results 8 Related Work 9 Conclusion References An Iterative Scheme of Safe Reinforcement Learning for Nonlinear Systems via Barrier Certificate Generation 1 Introduction 2 Preliminaries 3 Synthesis of Safe Controller via Learning and Verification 3.1 Training of Safe Controller 3.2 Safety Verification with Barrier Certificates 4 Algorithm 5 Experiments 6 Related Work 7 Conclusion References HYBRIDSYNCHAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL 1 Introduction 2 Preliminaries 3 The HYBRIDSYNCHAADL Modeling Language 4 The HYBRIDSYNCHAADL Tool 5 Case Study: Collaborating Autonomous Drones 6 Experimental Evaluation 7 Related Work 8 Concluding Remarks References Computing Bottom SCCs Symbolically Using Transition Guided Reduction 1 Introduction 2 Preliminaries 3 Basic Symbolic BSCC Detection 4 Transition Guided Reduction 5 Interleaved Transition Guided Reduction 6 Evaluation 6.1 Boolean Networks 6.2 Benchmark Set-Up 6.3 Real-World Networks 6.4 Pseudo-random Networks 6.5 Interleaving Performance Impact 7 Conclusions References Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems 1 Introduction 2 Overview of the Approach 3 Preliminaries 4 Explicit Computation of the Semi-Algebraic Abstraction 5 Linear Encoding of the Semi-Algebraic Abstraction 6 Experimental Evaluation 7 Related Work 8 Conclusions and Future Work References IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability 1 Introduction 2 An Expressive Input Language 3 A Variety of Synthesis Algorithms 4 Distribution 5 A Selection of Applications 6 Related Tools 7 Perspectives References Formally Verified Switching Logic for Recoverability of Aircraft Controller 1 Introduction 2 Related Work 3 Hybrid Controller Architecture 3.1 Aircraft Dynamics 3.2 LQR Controller 3.3 Switching Algorithm for the Safety of ANN Controller 4 Computation of Recoverable Zone 4.1 Under-Approximation of Recoverable Zone 5 Experimental Analysis 5.1 Experimental Setup 5.2 Experimental Results 5.3 Practical Challenges 6 Conclusions References SceneChecker: Boosting Scenario Verification Using Symmetry Abstractions 1 Introduction 2 Specifying Scenarios in SceneChecker 3 Transforming Scenarios to Hybrid Automata 4 Specifying Symmetry Maps in SceneChecker 5 Symmetry Abstraction of the Scenario's Automaton 6 SceneChecker Algorithm Overview 7 Experimental Evaluation 8 Limitations and Discussions References Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness 1 Introduction 2 Preliminaries 2.1 Hill Climbing-Guided Falsification 3 QB-Robustness 4 MCTS-Based Falsification Guided by QB-Robustness 4.1 MCTS Background 4.2 Proposed QB-Robustness-Guided Falsification Approach 5 Experimental Evaluation 5.1 Experiment Setup 5.2 Evaluation 6 Related Work 7 Conclusion and Future Work References Fast Zone-Based Algorithms for Reachability in Pushdown Timed Automata 1 Introduction 2 Preliminaries 2.1 Timed Automata 2.2 Reachability, Zones and Simulations 2.3 Pushdown Timed Automata (PDTA) 3 Zones in PDTA and the Problem with Simulations 4 Viewing Reachability Algorithms Using Rewrite Rules 4.1 Rewrite Rules for Timed Automata. 4.2 Rewrite Rules for PDTA 5 Algorithm for PDTA Reachability via Zones 6 Experiments and Results 7 Discussion and Future Work References Security Verified Cryptographic Code for Everybody 1 Introduction 1.1 Related Work 2 Project Design Constraints 3 AES-256-GCM and SHA-384 Proof Structure 4 SAW's Verification Pipeline 5 New Capability: x86 Semantics 6 New Capability: Verified Rewrites 6.1 Role of Rewrites in AES-256-GCM and SHA-384 Proofs 7 Results and Lessons Learned 7.1 Trade-Offs When Building on Existing Verification Tools 7.2 Verified Code Generation Versus Verifying Existing Code 8 Conclusion and Future Work References Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference 1 Introduction 2 Motivation 3 Background 4 Robust Reachability 4.1 Definition 4.2 Relation with Non-interference 4.3 Interpretation in Terms of Hyperproperty 4.4 Interpretation in Terms of Temporal Logic 4.5 Robust Reachability and Automatic Verification 5 Automatically Proving Robust Reachability 5.1 Robust Bounded Model Checking 5.2 Robust Symbolic Execution 5.3 Path Merging 5.4 Revisiting Standard Optimizations and Constructs 5.5 About Constraint Solving 6 Proof-of-Concept of a Robust Symbolic Execution Engine 6.1 Implementation 6.2 Case Studies: Exploitability Assessment for Vulnerabilities 6.3 Experimental Evaluation 6.4 Additional Considerations 7 Related Work 8 Conclusion A Details on the Experiments Supporting Sect.6.4 References A Temporal Logic for Asynchronous Hyperproperties 1 Introduction 2 Preliminaries 3 Asynchronous HyperLTL 3.1 Syntax and Semantics of Asynchronous HyperLTL 3.2 Examples of A-HLTL 4 Model-Checking A-HLTL 4.1 The Stuttering Construction 4.2 The Accelerating Construction 4.3 Decidable Practical A-HLTL Formulas 5 Undecidability and Lower-Bound Complexity 6 Case Studies and Evaluation 6.1 Compiler Optimizations 6.2 SPI Bus Protocol 7 Related Work 8 Conclusion References Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security 1 Introduction 2 Preliminaries 2.1 Noninterference 2.2 Modular Product Programs 3 Sound Products of IVL Encodings 3.1 Proposed Architecture 3.2 Soundness Issue 3.3 Soundness Criterion 3.4 Practical Relevance 3.5 Example: Dynamically-Bound Calls 4 Product Programs and Concurrency 4.1 Concurrent IVL Encodings 4.2 Possibilistic Noninterference 4.3 Probabilistic Noninterference 5 Implementation and Evaluation 5.1 Nagini 5.2 Performance Overhead of the Product Construction 5.3 Expressiveness and Comparison with SecC 6 Related Work 7 Conclusion References Constraint-Based Relational Verification 1 Introduction 2 Overview 2.1 Relational Verification Problems 2.2 Challenges and Contributions 3 Predicate Constraint Satisfaction Problems pfwCSP 4 Relational Verification with Constraints 4.1 k-Safety 4.2 Co-termination 4.3 Generalized Non-interference 5 Constraint Solving Method for pfwCSP 5.1 Predicate Synthesis with Stratified Families of Templates 6 Evaluation 7 Related Work 7.1 Relational Verification 7.2 Predicate Constraint Solving 8 Conclusion References Pre-deployment Security Assessment for Cloud Services Through Semantic Reasoning 1 Introduction 2 Preliminaries 3 Formalization and Encoding of IaC Deployments 4 Security Properties Specification 5 Application to Existing Infrastructure 5.1 Found Security Issues 6 Semantic Reasoning About Dataflows 7 Related Work 8 Conclusion and Future Work References Synthesis Synthesis with Asymptotic Resource Bounds 1 Introduction 2 Overview 2.1 Type-Directed Synthesis 2.2 Adding Resource Bounds 2.3 Checking Recurrence Relations 3 The SYNPLEXITY Type System 3.1 Syntax and Types 3.2 Semantics and Cost Model 3.3 Typing Rules 3.4 Soundness 4 The SynPlexity Synthesis Algorithm 4.1 Overview of the Synthesis Algorithm 5 Extensions to the SynPlexity Type System 6 Evaluation 6.1 Comparison to Prior Tools 6.2 Pruning the Search Space with Annotated Types 7 Related Work References Program Sketching by Automatically Generating Mocks from Tests 1 Introduction 2 Overview 3 The Sketcham Algorithm 4 Evaluation 4.1 Performance 4.2 Case Study: Deduplication 4.3 Discussion 5 Related Work 6 Conclusion References Counterexample-Guided Partial Bounding for Recursive Function Synthesis 1 Introduction 2 Background and Notation 3 Formal Definition of the Synthesis Problem 4 Recursion-Free Approximations 4.1 Partially Bounded Quantification 4.2 Refining Systems of Equations 5 Synthesis Algorithm 5.1 Expand : Producing Maximally Reducible Terms 5.2 Counterexample Generalization 5.3 Algorithm Properties 6 Implementation 6.1 Verification and Synthesis Oracles 6.2 Baseline Method 6.3 Optimizations 7 Evaluation 7.1 Case Studies 7.2 Experimental Results 8 Related Work 9 Discussion and Future Work References PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs 1 Introduction 2 Using PAYNT 3 Synthesis of Probabilistic Programs 4 Tool Architecture of PAYNT 5 Performance Evaluation and Applicability References Adapting Behaviors via Reactive Synthesis 1 Introduction 2 Preliminaries 3 Separated GR(k) Games 4 From Transducers to Separated GR(k) 4.1 Additional Usages of Our Technique 5 Overview for Solving Separated GR(k) Games 5.1 Algorithm Overview and Intuition 5.2 The Delay Property 6 Algorithms for Solving Separated GR(k) Games 6.1 Realizability and Synthesis for Weak Büchi Games 6.2 Realizability and Synthesis for Separated GR(k) Games 7 Implementation and Evaluation 8 Related Work 9 Conclusion References Causality-Based Game Solving 1 Introduction 2 Motivating Example 3 Preliminaries 4 Subgoals 5 Causality-Based Game Solving 5.1 Symbolically Represented Strategies 5.2 A Recursive Algorithm 5.3 Special Cases with Guaranteed Termination 6 Case Studies 6.1 Game of Nim 6.2 Corridor 6.3 Mona Lisa 6.4 Program Synthesis 7 Conclusion References Author Index