Verification, Model Checking, and Abstract Interpretation: 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16–21, 2020, ... Computer Science and General Issues)

Preface
Organization
Contents
Witnessing Secure Compilation
	1 Introduction
	2 Example
	3 Background
		3.1 Programs as Transition Systems
		3.2 Attack Models as Extended Transition Systems
		3.3 Büchi Automata over Trace Bundles
	4 Formulating Security Preservation
		4.1 Secure Program Transformation
	5 Refinement for Preservation of Universal Properties
	6 Checking Transformation Security
		6.1 Refinement Checking with SMT Solvers
		6.2 Refinement Relations for Compiler Optimizations
	7 Connections to Existing Proof Rules
		7.1 Constant Time
		7.2 Non-Interference
	8 Witnessing General Security Properties
		8.1 Checking General Refinement Relations
	9 Discussion and Related Work
	References
BackFlow: Backward Context-Sensitive Flow Reconstruction of Taint Analysis Results
	1 Introduction
		1.1 Contribution
		1.2 Running Example
	2 Related Work
	3 Formalization
		3.1 Language
		3.2 External Components
		3.3 Flow Reconstruction
		3.4 Backwards Propagation
	4 Integration with Julia
	5 Implementation
	6 Experimental Results
		6.1 Qualitative Study: WebGoat
		6.2 True Alarms
		6.3 False Alarms
		6.4 Quantitative Study: Benchmarks
	7 Conclusion
	References
Fixing Code that Explodes Under Symbolic Evaluation
	1 Introduction
	2 Overview
	3 Symbolic Performance Repair
		3.1 Repairs, Fixes, and Symbolic Cost
		3.2 The Symbolic Performance Repair Problem
	4 The SymFix Algorithm and Repairs
		4.1 Profile-Guided Search for Fixes
		4.2 Effective Repairs for Functional Hosts with Symbolic Reflection
		4.3 Implementation
	5 Evaluation
		5.1 Can SymFix Repair the Performance of State-of-the-Art Solver-Aided Tools, and How Do Its Fixes Compare to Experts\'?
		5.2 Do the Fixes Found by SymFix Generalize to Different Workloads?
		5.3 How Important Is SymFix\'s Search Strategy for Finding Fixes?
	6 Related Work
	7 Conclusion
	References
The Correctness of a Code Generator for a Functional Language
	1 Introduction
	2 A Small Functional Language
	3 Evaluation with Reference Counting
	4 A Small Imperative Language
	5 Conclusions
	References
Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
	1 Introduction
	2 Related Work
	3 SMACK Software Verification Toolchain
	4 Procedure for Adding a Language
		4.1 Interoperating with Language Models
		4.2 Compiling and Linking into Compiler IR
		4.3 Adding Models for Missing Language Features
	5 Case Studies
		5.1 Choice of Input Programming Languages
		5.2 Case Study 1: Microbenchmarks
		5.3 Case Study 2: Adding a Language
		5.4 Case Study 3: Cross-Language Verification
	6 Experience
		6.1 Trivially Supported Features
		6.2 Adding New Languages: Challenges and Solutions
		6.3 Cross-Language Verification
	7 Conclusions
	References
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
	1 Introduction
	2 Overview
	3 Verification by Induction over State Size
	4 Synthesizing Squeezing Functions
		4.1 Generate
		4.2 Test
		4.3 Filtering Out Unreachable States
	5 Implementation and Experimental Results
		5.1 Implementation
		5.2 Experimental Evaluation
	6 Related Work
	7 Conclusions
	References
A Systematic Approach to Abstract Interpretation of Program Transformations
	1 Introduction
	2 Illustrating Example: Singleton Analysis
		2.1 Abstract Interpreter for Program Transformations = Generic Interpreter + Term Abstraction
		2.2 A Singleton Term Abstraction
		2.3 Soundness
		2.4 Summary
	3 Generic Interpreters for Program Transformations
		3.1 The Program Transformation Language Stratego
		3.2 A Generic Interpreter for Stratego
		3.3 The Term Abstraction
	4 Sort Analysis
		4.1 Sorts and Sort Contexts
		4.2 Abstract Term Operations
		4.3 Sort Analysis and Generic Traversals
	5 Locally Ill-Sorted Sort Analysis
		5.1 Term Abstraction for Ill-Sorted Terms
		5.2 Abstract Term Operations
		5.3 Analyzing Type-Changing Generic Traversals
	6 Related Work
	7 Conclusion
	References
Sharing Ghost Variables in a Collection of Abstract Domains
	1 Introduction
	2 Related Work
	3 The Setup
	4 An Abstract Domain with Dynamic Support
		4.1 The Difficulties
		4.2 Ghost Variables and Constraints
		4.3 Generic Abstract Domain
		4.4 Running Ghost Constraints
		4.5 Non-interference
		4.6 Termination
		4.7 Support Unification
	5 Some Abstract Domains
		5.1 Pointers as Base + Offset
		5.2 Slices
		5.3 Numeric Domains: A Singular Case
		5.4 Linear Combinations
	6 Conclusion
	References
Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation
	1 Introduction
	2 Overview
	3 Programming Language
		3.1 Syntax
		3.2 Concrete Semantics
	4 Instrumented Semantics
		4.1 Instrumented States
		4.2 Instrumented Small-Step Operational Semantics
	5 Static Analysis
		5.1 Concretization
		5.2 Abstract Transformers
	6 Learning Pseudo-Inverse Functions
		6.1 Learning Transducers with OSTIA
		6.2 Needleman Wunsch Alignment Algorithm
	7 Implementation and Experimental Evaluation
	8 Related Work, Conclusion and Future Work
	References
Synthesizing Environment Invariants for Modular Hardware Verification
	1 Introduction
		1.1 Automatic Discovery of Environment Invariants
		1.2 SyGuS-Based Invariant Generation
	2 Background and Preliminaries
		2.1 Instruction-Level Modular Verification
		2.2 Checking Equivalence via Relational Program Verification
	3 Counterexample-Guided Invariant Synthesis
	4 SyGuS for Word-Level Invariant Synthesis
		4.1 Designing a Grammar for Environment Invariant Synthesis
		4.2 SyGuS Grammar
		4.3 Candidate Enumeration
		4.4 Enumerative SyGuS Solver
	5 Experimental Evaluation and Comparison
		5.1 Methods Evaluated
		5.2 Benchmark Examples
		5.3 Grammars Used for SyGuS
		5.4 Results of Experiments
		5.5 Detailed Comparison and Discussion
	6 Related Work
	7 Conclusions
	References
Systematic Classification of Attackers via Bounded Model Checking
	1 Introduction
	2 Preliminaries
	3 Motivational Example
	4 Bounded Model Checking of Compromised Systems
		4.1 Attackers and Compromised Systems
		4.2 A SAT Formula for BMC up to t Steps
		4.3 Isolation and Monotonicity
		4.4 Minimal (Successful) Attackers
		4.5 On Soundness and Completeness
		4.6 Requirement Clustering
	5 Evaluation
		5.1 Evaluating Methodologies
		5.2 Effectiveness of Isolation and Monotonicity
		5.3 Partial Classification of the pdtvsarmultip Benchmark
	6 Related Work
	7 Conclusion and Future Work
	References
Cheap CTL Compassion in NuSMV
	1 Introduction
		1.1 Our Contributions
	2 Making CTL Fair and Compassionate
	3 Streett-Fair CTL and the -Calculus
	4 NuSMV Implementation
		4.1 BDD-based Model Checking Within NuSMV
	5 Examples and Benchmarks
		5.1 Elevator Control System
		5.2 Non-emptiness for Random Büchi Automata
		5.3 Non-emptiness for Tree-Like Parity and Streett Automata
		5.4 Alternating Bit Protocol
	6 Conclusions
	References
A Cooperative Parallelization Approach for Property-Directed k-Induction
	1 Introduction
	2 Related Work
	3 Preliminaries
	4 The IcE/FiRE Framework
		4.1 Induction-Checking Engine
		4.2 Finite Reachability Engine
		4.3 Cooperation of Multiple Instances
	5 PD-KIND as an Instance of IcE/FiRE
		5.1 Induction-Checking Engine of PD-KIND
		5.2 Finite Reachability Engine of PD-KIND
		5.3 Parallel PD-KIND
	6 Implementation and Experiments
	7 Conclusions
	References
Generalized Property-Directed Reachability for Hybrid Systems
	1 Introduction
	2 Preliminary
	3 State-Transition Systems and Verification Problem
		3.1 Discrete-Time State-Transition Systems (DTSTS)
		3.2 Hybrid Automaton (HA)
		3.3 Safety Verification Problem
	4 GPDR for DTSTS
	5 HGPDR
		5.1 Extension of Forward Predicate Transformer
		5.2 Extension of GPDR
		5.3 Soundness
		5.4 Operational Presentation of HGPDR
	6 Proof-of-Concept Implementation
	7 Related Work
	8 Conclusion
	References
Language Inclusion for Finite Prime Event Structures
	1 Introduction
	2 Preliminaries
	3 Language Inclusion Problem and Complexity Results
		3.1 Language Membership Is NP-complete
		3.2 Language Inclusion Is p2-complete
	4 Deciding Language Inclusion
		4.1 Language Inclusion Decision Algorithm
		4.2 Automaton Based Language Inclusion
	5 Application and Evaluation
		5.1 Benchmarks and Results
	6 Related Work
	7 Conclusion and Future Work
	References
Promptness and Bounded Fairness in Concurrent and Parameterized Systems
	1 Introduction
	2 Prompt-LTLX  and Bounded Stutter Equivalence
		2.1 Prompt-LTLX
		2.2 Prompt-LTL and Stuttering
	3 Guarded Protocols and Parameterized Model Checking
		3.1 System Model: Guarded Protocols
		3.2 Parameterized Model Checking and Cutoffs
	4 Cutoffs for Disjunctive Systems
		4.1 Simulation up to Bounded Stutter Equivalence
		4.2 Cutoffs for Specifications in LTLX  Under Bounded Fairness
		4.3 Cutoffs for Specifications in Prompt-LTLX
	5 Cutoffs for Conjunctive Systems
		5.1 Cutoffs Under Local Bounded Fairness
		5.2 Cutoffs Under Global Bounded Fairness
	6 Token Passing Systems
		6.1 System Model
		6.2 Cutoff Results for Token Passing Systems
	7 Conclusions
	References
Solving LIA Using Approximations
	1 Introduction
	2 Linear Integer Arithmetic with the Star Operator
	3 Reasoning About Multisets as a LIA Problem
	4 Checking Satisfiability of LIA Formulas by Approximating from Above and Below
		4.1 Computing Over-Approximations of f
		4.2 Computing Under-Approximations of f
		4.3 Correctness
	5 Evaluation
	6 Related Work
	7 Conclusion
	References
Formalizing and Checking Multilevel Consistency
	1 Introduction
	2 Multilevel Consistency in the Wild
	3 Formalizing Multilevel Consistency
	4 Testing Multilevel Correctness of a Hybrid History
		4.1 Bad Pattern Characterization for Multilevel Correctness
		4.2 Constructing Minimal Visibility Relations
		4.3 Complexity
	5 Related Work
	References
Practical Abstractions for Automated Verification of Shared-Memory Concurrency
	1 Introduction
	2 Approach
	3 Formalisation
		3.1 Process Algebraic Models
		3.2 Programs
		3.3 Program Logic
		3.4 Entailment Rules
		3.5 Program Judgments
		3.6 Soundness
	4 Implementation
	5 Case Study
		5.1 Behavioural Specification
		5.2 Protocol Implementation
	6 Related Work
	7 Conclusion
	References
How to Win First-Order Safety Games
	1 Introduction
	2 First-Order Transition Systems
	3 First-Order Safety Games
	4 Monadic FO Safety Games
	5 Proving Invariants Inductive
	6 Hilbert\'s Choice Operator for Second Order Quantifiers
	7 Implementation
	8 Related Work
	9 Conclusion
	References
Improving Parity Game Solvers with Justifications
	1 Introduction
	2 Preliminaries
		2.1 Parity Games
		2.2 Nested Fixpoint Iteration for Parity Games
	3 Speeding up Fixpoint Iteration with Justifications
		3.1 Correctness
	4 Integrating Justifications in Other Algorithms
	5 Experimental Results
	6 Conclusion
	References
Author Index