Computer Aided Verification 33rd International Conference, CAV 2021, Virtual Event, July 20{u2013}23, 2021, Proceedings, Part I

This open access two-volume set LNCS 12759 and 12760 constitutes the refereed proceedings of the 33rd International Conference on Computer Aided Verification, CAV 2021, held virtually in July 2021. The 63 full papers presented together with 16 tool papers and 5 invited papers were carefully reviewed and selected from 290 submissions. The papers were organized in the following topical sections: Part I: invited papers; AI verification; concurrency and blockchain; hybrid and cyber-physical systems; security; and synthesis. Part II: complexity and termination; decision procedures and solvers; hardware and model checking; logical foundations; and software verification. This is an open access book. 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