Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part I

Preface
Organization
Contents – Part I
Contents – Part II
I AI Verification
NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
	1 Introduction
	2 Overview and Features
	3 Set Representations and Reachability Algorithms
		3.1 Polyhedron ch1tran2019parallel
		3.2 Star Set ch1tran2019fm,ch1tran2019emsoft (code)
		3.3 Zonotope ch1singh2018fast (code)
		3.4 Abstract Domain ch1singh2019abstract
		3.5 ImageStar Set ch1tran2020cav (code)
	4 Evaluation
		4.1 Safety Verification of ACAS Xu Networks
		4.2 Safety Verification of Adaptive Cruise Control System
	5 Related Work
	6 Conclusions
	References
Verification of Deep Convolutional Neural Networks Using ImageStars
	1 Introduction
	2 Problem Formulation
	3 ImageStar
	4 Reachability of CNN Using ImageStars
		4.1 Reachability of a Convolutional Layer
		4.2 Reachability of an Average Pooling Layer
		4.3 Reachability of a Fully Connected Layer
		4.4 Reachability of a Batch Normalization Layer
		4.5 Reachability of a Max Pooling Layer
		4.6 Reachability of a ReLU Layer
		4.7 Reachabilty Algorithm and Parallelization
	5 Evaluation
		5.1 Robustness Verification of MNIST Classification Networks
		5.2 Robustness Verification of VGG16 and VGG19
		5.3 Exact Analysis vs. Approximate Analysis
	6 Discussion
	7 Conclusion
	References
An Abstraction-Based Framework for Neural Network Verification
	1 Introduction
	2 Background
		2.1 Neural Networks
		2.2 Neural Network Verification
	3 Network Abstraction and Refinement
		3.1 Abstraction
		3.2 Refinement
	4 A CEGAR-Based Approach
		4.1 Generating an Initial Abstraction
		4.2 Performing the Refinement Step
	5 Implementation and Evaluation
	6 Related Work
	7 Conclusion
	References
Improved Geometric Path Enumeration for Verifying ReLU Neural Networks
	1 Introduction
	2 Background
		2.1 Neural Networks and Verification
		2.2 Basic Geometric Path Enumeration Algorithm
		2.3 Spatial Data Structures
		2.4 ACAS Xu Benchmarks
	3 Improvements
		3.1 Local Search Type (DFS vs BFS)
		3.2 Bounds for Splitting
		3.3 Fewer LPs with Concrete Simulations
		3.4 Zonotope Prefilter
		3.5 Eager Bounds Computation
		3.6 Zonotope Contraction
	4 Evaluation with Other Tools
	5 Related Work
	6 Conclusions
	A  Box Bounds Algorithm for Box-Halfspace Intersection
	B  Parallelization
	C  Full Optimization Data
	D  Full Tool Comparison Data
	References
Systematic Generation of Diverse Benchmarks for DNN Verification
	1 Motivation
	2 Background and Related Wok
	3 Identifying Factors that Influence Verifier Performance
		3.1 Potential Factors
		3.2 Exploratory Factor Study
	4 The GDVB Approach
		4.1 Factor Diverse Benchmarks
		4.2 From Factor Covering Arrays to Verification Problems
		4.3 Generating Benchmarks
		4.4 An Instantiation of GDVB
	5 GDVB in Use
		5.1 Setup
		5.2 Comparing Verifiers Across a Range of Challenges
		5.3 GDVB and Benchmark Requirements R1–R3
	6 Conclusion
	References
Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI
	1 Introduction
	2 Extensions of VerifAI
	3 TaxiNet Case Study
		3.1 Experimental Setup
		3.2 Falsification
		3.3 Error Analysis and Debugging
		3.4 Retraining
	4 Conclusion
	References
I Blockchain and Security
The Move Prover
	1 Introduction
	2 Background: The Move Language
	3 Tool Overview
	4 Boogie Model
	5 Specifications
	6 Evaluation
	7 Related Work
	8 Conclusion
	References
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
	1 Introduction
		1.1 Our Refinement-Based Verification Approach
	2 Formal Verification of the Deposit Contract
		2.1 Incremental Merkle Tree Algorithm
		2.2 Bytecode Verification of the Deposit Contract
	3 Findings and Lessons Learned
		3.1 Maximum Number of Deposits
		3.2 ABI Standard Conformance of get_deposit_count Function
		3.3 Checking Well-Formedness of Calldata
		3.4 Liveness
		3.5 Discussion
	4 Related Work
	References
Stratified Abstraction of Access Control Policies
	1 Introduction
	2 Overview
		2.1 Approach
		2.2 Solution: Computing Findings via Stratified Abstraction
	3 Algorithm
		3.1 Policies and Findings
		3.2 Properties
		3.3 Algorithm
	4 Implementation and Evaluation
	5 Related Work
	References
Synthesis of Super-Optimized Smart Contracts Using Max-SMT
	1 Introduction
	2 Overview: Optimal Bytecode as a Synthesis Problem
		2.1 Extracting Stack Functional Specifications from EVM Bytecode
		2.2 The Synthesis Problem
		2.3 Characteristics of Our SMT Encoding of the Synthesis Problem
		2.4 Optimal Synthesis Using Max-SMT
	3 Stack Functional Specification from EVM Bytecode
	4 Optimal Synthesis Using Max-SMT
		4.1 Abstracting Uninterpreted Functions
		4.2 Modeling the Stack
		4.3 Encoding of Instructions
		4.4 From Models to EVM Blocks
		4.5 Optimization Using Max-SMT
	5 Experimental Evaluation
		5.1 Comparison with ebso (setup I)
		5.2 Analysis of the Most Called Contracts with Gas Savings (setup Ii)
		5.3 Comparison of SMT Solvers in Precision and Time
	6 Related Work
	7 Conclusions and Future Work
	References
Verification of Quantitative Hyperproperties Using Trace Enumeration Relations
	1 Introduction
	2 Motivating Example
		2.1 Preliminaries
		2.2 Motivating Example: Zero-Knowledge Hats
		2.3 Solution Outline
	3 Overview of Quantitative Hyperproperties
		3.1 Quantitative Hyperproperties
		3.2 Applications of QHPs in Security Specification
	4 Trace Enumerations
		4.1 Trace Enumeration Relations
	5 Model Counting
		5.1 Model Counting via SMT Solving
		5.2 Model Counting in the Motivating Example
	6 Experimental Results and Discussion
		6.1 Methodology
		6.2 Overview of Results
		6.3 Deniability of Path ORAM
	7 Related Work
	8 Conclusion
	References
Validation of Abstract Side-Channel Models for Computer Architectures
	1 Introduction
	2 Background
		2.1 Observational Models
		2.2 The Evaluation Platform: Raspberry Pi 3
		2.3 Different Attacker and Observational Models
		2.4 Binary Intermediate Representation
	3 Program Generation
	4 Synthesis of Weakest Relation
	5 Test-Case Generation
	6 Implementation
	7 Results
		7.1 Direct-Mapped Cache Observational Model
		7.2 Partitioned Cache Observational Model
		7.3 Multi-way Cache Observational Model
		7.4 Problems in Model Implementations
	8 Related Work
	9 Concluding Remarks
	References
I Concurrency
Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
	1 Introduction
	2 Illustrative Example
	3 Semantics and Specifications
		3.1 Language Semantics
		3.2 Abstract Execution Semantics
		3.3 Replicated Store Semantics
		3.4 Correctness Specification
	4 Bounded Verification
		4.1 Vocabulary
		4.2 Implementation Constraints
		4.3 Abstract Execution Constraints
		4.4 Replicated Store Constraints
		4.5 Specification Constraints
	5 Experimental Evaluation
	6 Related Work and Conclusion
	References
Refinement for Structured Concurrent Programs
	1 Introduction
		1.1 Related Work
	2 Overview
		2.1 Yield Invariants
		2.2 Refining Atomic Actions
		2.3 Linear Interfaces
	3 RefPL: Syntax and Semantics
	4 Abstracting RefPL Programs
		4.1 Yield Invariants and Linear Interfaces
		4.2 Linearity
		4.3 Safety
		4.4 Refinement
	5 Implementation
	6 Conclusions
	References
Parameterized Verification of Systems with Global Synchronization and Guards
	1 Introduction
	2 System Model: Global Synchronization Protocols
		2.1 Global Synchronization Without Guards
		2.2 Global Synchronization with Guards
	3 Parameterized Verification for GSPs Without Guards
		3.1 Compatibility and Effective Computability of Predecessors
		3.2 Decidability for Unguarded GSPs
	4 Parameterized Verification for GSPs with Guards
		4.1 Guard-Compatibility and Well-Behaved Processes
		4.2 Decidability for Well-Behaved Guarded Processes
	5 Cutoffs for GSPs
		5.1 Definition and Basic Observations
		5.2 Conditions for Small Cutoffs
	6 Applications and Evaluation
	7 Related Work
	8 Conclusion
	References
HAMPA: Solver-Aided Recency-Aware Replication
	1 Introduction
	2 Recency-Aware Relational Object Language
	3 Coordination Conditions
	4 Replicated System Semantics
	5 Staleness Bound Inference and Optimization
	6 The Power and the Protocol of Recency-Aware Objects
	7 Experimental Results
	8 Related Work
	9 Conclusion
	References
Root Causing Linearizability Violations
	1 Introduction
	2 Overview
	3 Preliminaries
	4 Linearizability Violations and Their Root Causes
		4.1 Repair Oracle Approximation
		4.2 Generalization to Multiple Traces
	5 Conflict-Serializability Repairs
		5.1 Repairs and Conflict Cycles
		5.2 A Simple Algorithm
		5.3 A Sound Optimization
	6 Repair List Generation
		6.1 Optimal Repairs Enumeration Algorithm
		6.2 Ranking Optimal Repairs
	7 Experimental Evaluation
	8 Related Work
	References
Symbolic Partial-Order Execution for Testing Multi-Threaded Programs
	1 Introduction
	2 Overview
		2.1 Sequential Executions
		2.2 Independence Between Actions and Partial-Order Runs
		2.3 Unfolding: Merging the Partial Orders
		2.4 Exploring the Unfolding
		2.5 Cutoff Events: Pruning the Unfolding
	3 Main Algorithm
		3.1 Programs, Actions, and Runs
		3.2 Independence
		3.3 Partial-Order Runs
		3.4 Prime Event Structures
		3.5 Unfolding Semantics for Programs
		3.6 Conflicting Extensions
		3.7 Exploring the Unfolding
		3.8 Cutoffs and Completeness
	4 Implementation
		4.1 Standby States
		4.2 Hash-Based Cutoff Events
		4.3 Deterministic and Repeatable Allocations
		4.4 Data Race Detection
		4.5 External Function Calls
	5 Experimental Evaluation
		5.1 SV-COMP
		5.2 Memcached
		5.3 GNU sort
	6 Related Work
	7 Conclusion
	References
I Hardware Verification and Decision Procedures
fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components
	1 Introduction
	2 Design
		2.1 Frontend: Tester API
		2.2 Actions IR
		2.3 Backend Targets
	3 Evaluation
	4 Related Work
	5 Conclusion
	References
Nonlinear Craig Interpolant Generation
	1 Introduction
	2 Preliminaries
		2.1 Quadratic Module
		2.2 Problem Description
	3 Existence of Interpolants
	4 SOS Formulation
	5 Avoidance of the Unsoundness Due to Numerical Error in SDP
	6 Generalizing to General Polynomial Formulas
	7 Application to Invariant Generation
	8 Conclusion
	References
Approximate Counting of Minimal Unsatisfiable Subsets
	1 Introduction
	2 Preliminaries and Problem Formulation
		2.1 Problem Definitions
	3 Related Work
	4 AMUSIC: A Hashing-Based MUS Counter
		4.1 Algorithmic Overview
		4.2 Analysis and Comparison with ApproxMC3
		4.3 Counting MUSes in a Cell: CountInCell
		4.4 Computing UMUF
		4.5 Computing IMUG
	5 Experimental Evaluation
	6 Summary and Future Work
	References
Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and Sampling
	1 Introduction
	2 Notations and Preliminaries
	3 Background
		3.1 Hashing-Based Model Counting
		3.2 Hashing-Based Sampling
		3.3 The Underlying SAT Solver
	4 Technical Contributions to CNF-XOR Solving
		4.1 Detaching XOR Clauses from Watch-Lists
		4.2 Fast Propagation/Conflict Detection and Reason Generation
		4.3 Lazy Reason Clause Generation
		4.4 Skipping Solution Extension of Eliminated Variables
		4.5 Putting It All Together: BIRD2
	5 Technical Contribution to Counting and Sampling
		5.1 Reuse of Previously Found Solutions
		5.2 ApproxMC4 and UniGen3
	6 Evaluation
		6.1 Performance
		6.2 Quality and Correctness
	7 Conclusions
	References
Automated and Scalable Verification of Integer Multipliers
	1 Introduction
	2 Preliminaries
		2.1 ACL2 and Term Rewriting
		2.2 Semantics for Hardware Designs
		2.3 Multiplier Architectures
	3 Specification
	4 Methodology
		4.1 Adder Module Proofs
		4.2 Multiplier Module Proofs
	5 Termination
		5.1 Measure for Adder Module Simplification
		5.2 Measure for Multiplier Module Simplification
	6 Experiments
	7 Related Work and Conclusion
	References
Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing
	1 Introduction
	2 Preliminaries
	3 Semantic Gate Extraction by Interpolation
	4 Extracting Unique QBF Strategy Functions
		4.1 An Algorithm for Computing Unique Strategy Functions
		4.2 Improvements and Generalization to Dependency QBF
	5 Implementation
	6 Experiments
		6.1 Gate Extraction
		6.2 Solving Formulas Augmented with Definitions
	7 Related Work
	8 Conclusion
	References
TARTAR: A Timed Automata Repair Tool
	1 Introduction
	2 New Types of Repair Analyses
	3 Usage of TarTar
	4 Software Architecture and Implementation of TarTar
	5 Evaluation
	6 Conclusion
	References
I Hybrid and Dynamic Systems
SAW: A Tool for Safety Analysis of Weakly-Hard Systems
	1 Introduction
	2 Algorithms and Tool Design
		2.1 Reachability Graph Construction
		2.2 DP-Based Local Safety Set Search
		2.3 Reverse Inductiveness Set Search
	3 Example Usage
	4 Experiments
		4.1 Comparison with One-Dimension Abstraction
		4.2 Impact of (m,K), Granularity, and Stepsize
	5 Conclusion
	References
PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems
	1 Introduction
	2 Interval Reachability Analysis
		2.1 Methods to Compute Interval Reachable Sets
	3 Parallelization
	4 Complexity of the Parallelized Methods
	5 Case Studies
		5.1 n-link Road Traffic Model
		5.2 Quadrotor Swarm
		5.3 Quadrotor Swarm with Artificial Potential Field
		5.4 Heat Diffusion
		5.5 Overtaking Maneuver with a Single-Track Vehicle
		5.6 Performance on ARCH Benchmarks
	6 Conclusion
	References
AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks
	1 Introduction
	2 Attractors in Parametrised Boolean Networks
	3 Attractor Bifurcation Analysis with AEON
	4 Implementation
	5 Evaluation
	References
A Novel Approach for Solving the BMI Problem in Barrier Certificates Generation
	1 Introduction
	2 Preliminaries
	3 Transfer to BMI
	4 A Sequential Iterative Scheme for Solving BMI Problems
		4.1 An Iterative Scheme
		4.2 Analytical Solutions for the Sequential Iteration
		4.3 Algorithm and Complexity Analysis
	5 Experiments
	6 Related Work
	7 Conclusion
	References
Reachability Analysis Using Message Passing over Tree Decompositions
	1 Introduction
		1.1 Related Work
	2 Preliminaries
		2.1 Tree Decomposition
	3 Abstract Domains Using Tree Decompositions
		3.1 Abstraction and Concretization
		3.2 Canonical Elements and Message Passing
		3.3 Decomposable Sets and Post-conditions
	4 Grid-Based Interval Analysis
		4.1 Tree Decomposed Analysis
	5 Experimental Evaluation
	6 Conclusions
	References
Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models
	1 Introduction
	2 Preliminaries and Problem Statement
		2.1 Nonlinear Control System
		2.2 Controller Synthesis Problem
	3 Constructing Reference Trajectories from Waypoints
	4 Bounding the Error of a Tracking Controller
		4.1 Tracking Error and Lyapunov Functions
		4.2 Bounding Tracking Error Using Lyapunov Functions: Part 1
		4.3 Bounding Tracking Error Using Lyapunov Functions: Part 2
	5 Synthesizing the Reference Trajectories
		5.1 Use PWL Reference Trajectories for Vehicle Models
		5.2 Synthesizing Waypoints for a Linear Reference Trajectory
		5.3 Partitioning the Initial Set
		5.4 Overall Synthesis Algorithm
	6 Implementation and Evaluation
		6.1 Benchmark Scenarios: Vehicle Models and Workspaces
		6.2 Synthesis Performance
		6.3 RRT vs. SAT-Plan
	7 Conclusion and Discussion
	References
SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks
	1 Introduction
	2 Workflow and Key Functionality
		2.1 Semi-quantitative Abstraction
		2.2 Semi-quantitative Analysis
		2.3 Visualization of Qualitative Information
		2.4 Visualization of Quantitative Information
		2.5 Precision and Refinement
		2.6 Mean Simulations
	3 Conclusion
	References
Author Index