Computer Aided Verification: 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II

Preface
Organization
Contents – Part I
Contents -- Part II
Invited Papers
Semantic Adversarial Deep Learning
	1 Introduction
	2 Background
	3 Attacks
		3.1 Test-Time Attacks
		3.2 Adversarial Training
		3.3 Black Box Attacks
		3.4 Defenses
	4 Semantic Adversarial Analysis and Training
		4.1 Compositional Falsification
		4.2 Semantic Training
	5 Conclusion
	References
From Programs to Interpretable Deep Models and Back
	1 Introduction
		1.1 Motivating Tasks
	2 From Programs to Deep Models
		2.1 Representation
		2.2 Code2vec: Learning Code Embeddings
		2.3 Code2seq: Generating Sequences from Structured Representations of Code
	3 From Deep Models to Automata
		3.1 What Has a Network Learned?
		3.2 Counterexamples
	4 Conclusion
	References
Formal Reasoning About the Security of Amazon Web Services
	1 Introduction
	2 Security of the Cloud
	3 Securing Customers in the Cloud
	4 Challenges
	5 Conclusion
	References
Tutorials
Foundations and Tools for the Static Analysis of Ethereum Smart Contracts
	1 Introduction
	2 Background on Ethereum
		2.1 Ethereum
		2.2 EVM Bytecode
	3 Overview on Formal Verification Approaches
		3.1 Verification
		3.2 Design
		3.3 Open Challenges
	4 Semantics
		4.1 Execution Configurations
		4.2 Small-Step Rules
	5 Security Properties
		5.1 Preliminary Notations
		5.2 Single-Entrancy
	6 Verification
		6.1 Abstract Semantics
		6.2 Abstract Configurations
		6.3 Abstract Execution Rules
	7 Verifying Security Properties
		7.1 Over-Approximating Single-Entrancy
		7.2 Examples
		7.3 Discussion
	8 Conclusion
	References
Layered Concurrent Programs
	1 Introduction
		1.1 Related Work
	2 Concurrent Programs
		2.1 Running Example
	3 Layered Concurrent Programs
		3.1 Type Checker
		3.2 Concurrent Program Extraction
		3.3 Running Example
	4 Refinement Checking
		4.1 From Preemptive to Cooperative Semantics
		4.2 Refinement Checker Programs
	5 Conclusion
	References
Model Checking
Propositional Dynamic Logic for Higher-Order Functional Programs
	1 Introduction
	2 Higher-Order Traces
		2.1 Trace Semantics for Higher-Order Functional Programs
	3 Propositional Dynamic Logic over Higher-Order Traces
	4 Applications of HOT-PDL
		4.1 Dependent Refinement Types
		4.2 Stack-Based Access Control Properties
	5 HOT-PDL Model Checking
	6 Related Work
	7 Conclusion and Future Work
	References
Syntax-Guided Termination Analysis
	1 Introduction
	2 Background and Notation
	3 Exploiting Program Syntax
	4 Proving Termination
		4.1 Synthesizing Linear Termination Arguments
		4.2 Synthesizing Lexicographic Termination Arguments
	5 Proving Non-termination
		5.1 Synthesizing Non-terminating Refinements
		5.2 Integrating Algorithms Together
	6 Evaluation
		6.1 Performance on Terminating Benchmarks
		6.2 Performance on Non-terminating Benchmarks
		6.3 Large-Scale Benchmarks
	7 Related Work
	8 Conclusion
	References
Model Checking Quantitative Hyperproperties
	1 Introduction
		1.1 Related Work
	2 Preliminaries
		2.1 HyperLTL
		2.2 System Model
		2.3 Automata over Infinite Words
	3 Quantitative Hyperproperties
	4 Model Checking Quantitative Hyperproperties
		4.1 Standard Model Checking Algorithm: Encoding Quantitative Hyperproperties in HyperLTL
		4.2 Counting-Based Model Checking Algorithm
		4.3 Büchi Automata for Quantitative Hyperproperties
		4.4 Counting Models of -Automata
	5 A Max#Sat-Based Approach
		5.1 Experiments
	6 Conclusion
	References
Exploiting Synchrony and Symmetry in Relational Verification
	1 Introduction
	2 Motivating Example
	3 Background and Notation
	4 Leveraging Relational Specifications
		4.1 Synchronizing Loops
		4.2 Synchronizing Conditionals
		4.3 Discovering and Exploiting Symmetries
	5 Instantiation of Strategies in Forward Analysis
	6 Implementation and Evaluation
		6.1 Stackoverflow Benchmarks
		6.2 Modified Stackoverflow Benchmarks
	7 Related Work
	8 Conclusions and Future Work
	References
JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
	1 Introduction
	2 JBMC: A Bounded Model Checker for Java Bytecode
		2.1 Architecture and Implementation
		2.2 Java Operational Model
		2.3 String Solver
		2.4 JBMC Usage
	3 Experimental Evaluation
		3.1 Objectives and Setup
		3.2 Results
	4 Conclusions and Future Work
	References
Eager Abstraction for Symbolic Model Checking
	1 Introduction
	2 Preliminaries
	3 A Schema-Based Abstraction Class
	4 Example Abstractions in the Class
	5 Proof Methodology
	6 Case Studies
	7 Conclusion
	References
Program Analysis Using Polyhedra
Fast Numerical Program Analysis with Reinforcement Learning
	1 Introduction
	2 Reinforcement Learning for Static Analysis
		2.1 Reinforcement Learning
		2.2 Instantiation of RL to Static Analysis
	3 Polyhedra Analysis and Approximate Transformers
		3.1 Polyhedra Analysis
		3.2 Online Decomposition
		3.3 Approximating the Polyhedra Join
	4 Reinforcement Learning for Polyhedra Analysis
	5 Experimental Evaluation
	6 Related Work
	7 Conclusion
	References
A Direct Encoding for NNC Polyhedra
	1 Introduction
	2 Preliminaries
	3 Direct Representations for NNC Polyhedra
	4 The New Conversion Algorithm
		4.1 Processing the Skeleton
		4.2 Processing the Non-skeleton
		4.3 Duality
	5 Experimental Evaluation
	6 Conclusion
	References
Synthesis
What's Hard About Boolean Functional Synthesis?
	1 Introduction
	2 Notations and Problem Statement
	3 Complexity-Theoretical Limits
	4 Phase 1: Efficient Polynomial-Sized Synthesis
	5 Phase 2: Counterexample-Guided Refinement
	6 Experimental Results
	7 Conclusion
	References
Counterexample Guided Inductive Synthesis Modulo Theories
	1 Introduction
	2 Preliminaries
		2.1 The Program Synthesis Problem
		2.2 CounterExample Guided Inductive Synthesis
		2.3 DPLL(T)
	3 Motivating Example
	4 CEGIS(T)
		4.1 Overview
		4.2 CEGIS(T) with a Theory Solver Based on FM Elimination
		4.3 CEGIS(T) with an SMT-based Theory Solver
	5 Experimental Evaluation
		5.1 Implementation
		5.2 Benchmarks
		5.3 Experimental Setup
		5.4 Results
		5.5 Threats to Validity
	6 Related Work
	7 Conclusion
	References
Synthesizing Reactive Systems from Hyperproperties
	1 Introduction
	2 Preliminaries
	3 HyperLTL Synthesis
	4 Bounded Realizability
	5 Bounded Unrealizability
	6 Evaluation
	7 Conclusion
	References
Reactive Control Improvisation
	1 Introduction
	2 Background
		2.1 Notation
		2.2 Synthesis Games
	3 Problem Definition
		3.1 Motivating Example
		3.2 Reactive Control Improvisation
	4 Existence of Improvisers
		4.1 Width and Realizability
		4.2 Improviser Construction: Discussion
		4.3 Improviser Construction: Details
	5 A Generic Improviser
	6 Reachability Games and DFAs
	7 Temporal Logics and Other Specifications
	8 Conclusion
	References
Constraint-Based Synthesis of Coupling Proofs
	1 Introduction
	2 Overview and Illustration
		2.1 Introducing f-Couplings
		2.2 Simulating a Fair Coin
	3 A Proof Rule for Coupling Proofs
		3.1 Distributions and Couplings
		3.2 Program Model
		3.3 Coupled Postconditions
		3.4 Proof Rules for Uniformity and Independence
	4 Constraint-Based Formulation of Proof Rules
		4.1 Generating Logical and Probabilistic Constraints
		4.2 Constraint Transformation
	5 Dealing with Loops
	6 Implementation and Evaluation
	7 Related Work
	References
Controller Synthesis Made Real: Reach-Avoid Specifications and Linear Dynamics
	1 Introduction
	2 Preliminaries and Problem Statement
		2.1 Discrete Time Linear Control Systems
		2.2 Bounded Controller Synthesis Problem
	3 Synthesis Algorithm
		3.1 Overview
		3.2 Synthesizing the Tracking Controller K
		3.3 Reachset Over-Approximation with Tracking Controller
		3.4 Shaping Ellipsoids for Tight Over-Approximating Hyper-rectangles
		3.5 Synthesis of Open-Loop Controller
		3.6 Synthesis Algorithm Putting It All Together
	4 RealSyn Implementation and Evaluation
		4.1 Implementation
		4.2 Evaluation
	5 Conclusion
	References
Synthesis of Asynchronous Reactive Programs from Temporal Specifications
	1 Introduction
	2 Preliminaries
	3 Symbolic Asynchronous Synthesis
		3.1 Basic Formulations and Properties
		3.2 The Pnueli-Rosner Closure
		3.3 The Closure Automaton Construction
		3.4 Symbolic Construction
	4 Implementation and Experiments
	5 Efficiently Solvable Subclasses of LTL
	6 Conclusions and Related Work
	References
Syntax-Guided Synthesis with Quantitative Syntactic Objectives
	1 Introduction
	2 Illustrative Example
	3 SyGuS with Quantitative Objectives
		3.1 Weights over Semirings
		3.2 Weighted Tree Grammars
		3.3 QSyGuS
	4 Solving QSyGuS Problems via Grammar Reduction
		4.1 From QSyGuS to SyGuS
		4.2 Finding an Optimal Solution
	5 Implementation and Evaluation
		5.1 Effectiveness of QSyGuS Solver
		5.2 Solving Time for Different Iterations
		5.3 Solution Weight Across Iterations
		5.4 Multi-objective Optimization
	6 Related Work
	7 Conclusion
	References
Learning
Learning Abstractions for Program Synthesis
	1 Introduction
	2 Illustrative Example
	3 Overall Abstraction Learning Algorithm
	4 Learning Abstract Domain Using Tree Interpolation
	5 Synthesis of Abstract Transformers
		5.1 Example Generation
	6 Soundness and Completeness
	7 Implementation and Evaluation
		7.1 Abstraction Learning
		7.2 Evaluating the Usefulness of Learned Abstractions
	8 Related Work
	9 Limitations
	10 Conclusion
	References
The Learnability of Symbolic Automata
	1 Introduction
	2 Background
		2.1 Boolean Algebras and Symbolic Automata
		2.2 Learning Model
	3 The MAT* Algorithm
		3.1 The Classification Tree
		3.2 Building an s-FA Model
		3.3 Processing Counterexamples
	4 Correctness and Completeness of MAT*
	5 Learnable Boolean Algebras
	6 Evaluation
		6.1 Equality Algebra Learning
		6.2 BDD Algebra Learning
		6.3 s-FA Algebra Learning
	7 Related Work
	References
Runtime Verification, Hybrid and Timed Systems
Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes
	1 Introduction
	2 Preliminaries
	3 Computing Barrier Certificates
	4 Piecewise Barrier Tubes
		4.1 Constructing an Enclosure Box
		4.2 Compute a Barrier Tube Inside a Box
		4.3 Compute Piecewise Barrier Tube
	5 Implementation and Experiments
	6 Conclusion
	References
Space-Time Interpolants
	1 Introduction
	2 Motivating Example
	3 Hybrid Automata with Piecewise Affine Dynamics
	4 Time Abstraction Using Interval Arithmetic
		4.1 Continuous Dynamics
		4.2 Hybrid Dynamics
	5 Space Abstraction Using Support Functions
		5.1 Support Functions
		5.2 Computing Template Polyhedra
	6 Abstraction Refinement Using Space-Time Interpolants
		6.1 Halfspace Interpolation
		6.2 Time Partitioning
		6.3 Abstraction Refinement
	7 Experimental Evaluation
	8 Related Work
	9 Conclusion
	References
Monitoring Weak Consistency
	1 Introduction
	2 Weak Consistency
	3 Minimal Visibility Extensions
	4 Efficient Monitoring of Consistency Models
	5 Empirical Results
	6 Related Work
	7 Conclusion
	References
Monitoring CTMCs by Multi-clock Timed Automata
	1 Introduction
	2 Preliminaries
		2.1 Continuous-Time Markov Chain (CTMC)
		2.2 Deterministic Timed Automaton (DTA)
		2.3 Piecewise-Deterministic Markov Process (PDP)
	3 Reduction to the Reachability Probability of EPDP
	4 Approximating the Reachability Probability of EPDP
		4.1 Reduction to a PDE System
		4.2 Reduction to an ODE System
		4.3 Numerical Solution
		4.4 Complexity Analysis
	5 Experimental Results
	6 Concluding Remarks
	References
Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
	1 Introduction
	2 Partial Order Reduction for Timed Systems
	3 Timed-Arc Petri Nets
		3.1 Reachability Logic and Interesting Sets of Transitions
	4 Partial Order Reductions for TAPN
	5 Implementation and Experiments
	6 Conclusion
	References
A Counting Semantics for Monitoring LTL Specifications over Finite Traces
	1 Introduction
	2 Related Work
	3 Preliminaries
	4 Counting Finitary Semantics for LTL
		4.1 Definitions
		4.2 Semantics
		4.3 Evaluation
	5 Examples
	6 Conclusion
	References
Tools
Rabinizer 4: From LTL to Your Favourite Deterministic Automaton
	1 Introduction
	2 Functionality
		2.1 Translations
		2.2 Verification and Synthesis
	3 Optimizations, Implementation, and Evaluation
	4 Conclusion
	References
Strix: Explicit Reactive Synthesis Strikes Back!
	1 Introduction
	2 Design and Implementation
	3 Experimental Evaluation
		3.1 Effects of Minimization
		3.2 Synthesis of Complete AMBA AHB Arbiter
		3.3 Discussion
	References
BTOR2 , BtorMC and Boolector 3.0
	1 Format Description
	2 Sequential Extension
	3 Witness Format
	4 Tools
	5 Experiments
	6 Conclusion
	References
Nagini: A Static Verifier for Python
	1 Introduction
	2 Language and Specifications
	3 Implementation
	4 Evaluation
	References
Peregrine: A Tool for the Analysis of Population Protocols
	1 Introduction
	2 Population Protocols
	3 Analyzing Population Protocols
	References
ADAC: Automated Design of Approximate Circuits
	1 Introduction
	2 Architecture and Implementation
	3 Evaluation, Related Works, and Applications
	References
Probabilistic Systems
Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
	1 Introduction
	2 Preliminaries
		2.1 Basic Definitions
		2.2 (Bounded) Value Iteration
	3 Example
	4 Convergent Over-Approximation
		4.1 Bloated End Components Cause Non-convergence
		4.2 Static MSEC Decomposition
		4.3 Dynamic MSEC Decomposition
		4.4 Learning-Based Algorithm
	5 Experimental Results
	6 Conclusions
	References
Sound Value Iteration
	1 Introduction
	2 Preliminaries
		2.1 Probabilistic Models and Measures
		2.2 Probabilistic Model Checking via Interval Iteration
	3 Sound Value Iteration for MCs
		3.1 Approximating Reachability Probabilities
		3.2 Extending the Value Iteration Approach
		3.3 Sound Value Iteration for Expected Rewards
		3.4 Optimizations
	4 Sound Value Iteration for MDPs
		4.1 Approximating Maximal Reachability Probabilities
		4.2 Extending the Value Iteration Approach
	5 Experimental Evaluation
	6 Conclusion
	References
Safety-Aware Apprenticeship Learning
	1 Introduction
	2 Preliminaries
		2.1 Markov Decision Process and Discrete-Time Markov Chain
		2.2 Apprenticeship Learning via Inverse Reinforcement Learning
		2.3 PCTL Model Checking
	3 Problem Formulation and Overview
	4 A Framework for Safety-Aware Learning
	5 Counterexample-Guided Apprenticeship Learning
	6 Experiments
		6.1 Grid World
		6.2 Cart-Pole from OpenAI Gym
		6.3 Mountain-Car from OpenAI Gym
	7 Related Work
	8 Conclusion and Future Work
	References
Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains
	1 Introduction
	2 Labelled Markov Chains and Probabilistic Bisimilarity Distances
	3 Distance One
	4 Distance Smaller Than One
	5 Number of Non-trivial Distances
	6 All Distances
	7 Small Distances
	8 Approximation Algorithm
	9 Conclusion
	References
Author Index