Verification, Model Checking, and Abstract Interpretation: 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021, Proceedings (Lecture Notes in Computer Science)

This book constitutes the proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021, which was held virtually during January 17-19, 2021. The conference was planned to take place in Copenhagen, Denmark, but changed to an online event due to the COVID-19 pandemic. The 23 papers presented in this volume were carefully reviewed from 48 submissions. VMCAI provides a forum for researchers working on verification, model checking, and abstract interpretation and facilitates interaction, cross-fertilization, and advancement of hybrid methods that combine these and related areas. The papers presented in this volume were organized in the following topical sections: hyperproperties and infinite-state systems; concurrent and distributed systems; checking; synthesis and repair; applications; and decision procedures. Preface Organization Contents Invited Papers Model Checking Algorithms for Hyperproperties (Invited Paper) 1 Introduction 2 HyperLTL 3 HyperQPTL 4 Beyond HyperQPTL 5 HyperCTL* 6 HyperQCTL* 7 Monadic Path Logic 8 Conclusions References Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper) 1 Introduction 2 Motivating Examples for Synthesising Invariants and Loops 3 Algebra-Based Synthesis of Loop Invariants 4 Algebra-Based Synthesis of Loops 5 Conclusions References Generative Program Analysis and Beyond: The Power of Domain-Specific Languages (Invited Paper) 1 Introduction 2 The LTL Mindset 3 The SOS Mindset 3.1 Standard SOS 3.2 Control Flow Analysis: The One Point Domain 3.3 Property Oriented Expansion via SOS 4 The Modal Meta Mindset 5 Conclusions and Perspectives References Hyperproperties and Infinite-State Systems Compositional Model Checking for Multi-properties 1 Introduction 2 Preliminaries 2.1 Hyperproperties and HyperLTL 3 Multi-models and Multi-properties 3.1 Examples 3.2 Model-Checking MultiLTL 4 Compositional Proof Rules for Model-Checking MultiLTL 5 Abstraction-Refinement Based Implementation of ([ProofRule]PR) and ([NegProofRule]PR) 5.1 Constructing a Sequence of Over-Approximations 5.2 Constructing a Sequence of Under-Approximations 5.3 Abstraction-Refinement Guided MultiLTL Model-Checking Using ([ProofRule]PR) and ([NegProofRule]PR) 5.4 Counterexample Guided MultiLTL Model-Checking Using ([ProofRule]PR) 6 Multi-properties for Finite Traces 6.1 Multi-languages and Multi-NFH 7 Learning-Based Multi-property Model-Checking 7.1 Learning Assumptions for General Multi-properties 7.2 Weakest Assumption for 7.3 Learning Assumptions for 8 Conclusion References Decomposing Data Structure Commutativity Proofs with mn-Differencing 1 Introduction 2 Overview 3 Preliminaries 4 One-Shot Reduction to Reachability 5 Decomposing Commutativity with mn-differencing 5.1 Formal Definition 5.2 Connecting the Pieces Together 6 mn-differencing for Automata-Based Verification 7 Evaluation 8 Related Work 9 Discussion and Future Work References Proving the Existence of Fair Paths in Infinite-State Systems 1 Introduction 2 Background 3 Running Example 4 Fair Paths: Sufficient Conditions 4.1 Comparison with Recurrent Sets 5 Decomposition of the Sufficient Conditions 5.1 Example: Decomposition 6 Search of the Composition 7 Ensuring Divergence of a Given Symbol 7.1 Example: Diverging ``Time'' 8 Related Work 9 Experimental Evaluation 10 Conclusions References A Self-certifying Compilation Framework for WebAssembly 1 Introduction 2 Overview 3 WebAssembly: Syntax and Semantics 3.1 The WebAssembly Instruction Set 3.2 WebAssembly Semantics 4 Witness Structure and Validation 5 Proof Generation 6 Validator Implementation 6.1 Encoding into SMT 6.2 Evaluation 7 Related Work and Conclusions References Concurrent and Distributed Systems Concurrent Correctness in Vector Space 1 Introduction 2 System Model 3 Methodology 3.1 Correctness Defined in Vector Space 4 Dynamic Correctness Tool Implementation 4.1 Time Complexity 4.2 Correctness 5 Discussion 6 Experimental Evaluation 6.1 Enhancements Using the GPU 7 Related Work 7.1 Comparison of the Proposed Dynamic Analysis Tool to Existing Tools 8 Conclusion References Verification of Concurrent Programs Using Petri Net Unfoldings 1 Introduction 2 Examples 2.1 Retaining Concurrency of Different Threads 2.2 Adding Synchronization Lazily 3 Petri Net and Finite Automata 3.1 Finite Automata 3.2 Petri Nets as Language Acceptors 4 Petri Programs 4.1 Program Semantics 4.2 Verification Problem 5 Verification Algorithm 6 Difference Operation 7 Discussion 8 Related Work 9 Conclusion References Eliminating Message Counters in Synchronous Threshold Automata 1 Introduction 2 Our Approach at a Glance 3 Synchronous Threshold Automata 3.1 Receive Synchronous Threshold Automata 3.2 Environment Assumption and Modeling Faults 4 Counter Systems 5 Synchronous Transition Systems 6 Abstracting rSTA to STA 6.1 Guard Strengthening 6.2 Eliminating the Receive Variables 6.3 Soundness and Completeness 7 Experimental Evaluation 8 Conclusions References A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries 1 Introduction 2 Modeling Randomized Threshold-Based Algorithms 2.1 Symmetry in PTAP 2.2 Semantics of a PTAP 2.3 Message Identities 2.4 Adversaries 2.5 Atomic Propositions and Stutter Equivalence 3 Reduction to Communication-Closed Adversaries 4 From Weak to Round-Rigid Adversaries 5 Conclusions References Abstract Interpretation and Model Checking Runtime Abstract Interpretation for Numerical Accuracy and Robustness 1 Introduction 2 Motivating Numerical Example 3 Overview of Runtime Abstract Interpretation 4 The RAI Technique in More Detail 4.1 Primitives to Express Numerical Properties 4.2 Propagating Abstract Values at Runtime 4.3 Covering All Executions for Unstable Tests 5 Experimental Results 6 Related Work 7 Conclusion and Perspectives References Twinning Automata and Regular Expressions for String Static Analysis 1 Introduction 1.1 Related Work 2 Motivating Example 3 Preliminaries 4 The Tarsis abstract domain 4.1 Abstract Domain and Widening 4.2 String Abstract Semantics of Imp 5 Experimental Results 5.1 Precision of the Various Domains on Test Cases 5.2 Evaluation on Realistic Code Samples 5.3 Efficiency 6 Conclusion References Unbounded Procedure Summaries from Bounded Environments 1 Introduction 2 Motivating Example 2.1 Using the Program Call Graph 2.2 Summary Updates Using SMT Queries 2.3 Explicit Induction and EC lemmas 3 Preliminaries 4 Bounded Contexts and Environments 5 EC Lemmas 6 Modular Verification Algorithm 6.1 Algorithm Outline 6.2 Proof Rules Without Induction 6.3 Ordering and Conditions for SMT Queries 6.4 Proof Rules for Induction 6.5 Correctness and Progress 7 Evaluation and Results 7.1 Description of Benchmarks 7.2 Results and Discussion 8 Related Work 8.1 CHC-solving for Program Verification 8.2 Program Analysis and Verification 8.3 Specification Inference 9 Conclusions A Renaming and Unfolding B Full Set of Derivation Rules C Heuristics C.1 Prioritizing Choice of Node C.2 Avoiding Redundant Queries C.3 Learning Over-approximate Bodies C.4 Preventing Summaries from Growing too Large D Addition of Nodes in Derivation Tree E Correctness and Progress Proof Sketches F Additional Experimental Results References Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking 1 Introduction 2 Background and Notation 2.1 Constrained Horn Clauses (CHCs) 2.2 Hardware Model Checking Using CHCs 2.3 IC3/PDR and APDR 2.4 CHC Solving Techniques for Bit-Vectors 3 A Motivating Example 4 Integrating SyGuS with IC3/PDR 4.1 Lemma Formulation 4.2 SyGuS-Based Interpolation 4.3 Lemma Generation and Validation 4.4 Generating Terms in the Grammar 4.5 Tightening Previous Frames in IC3/PDR 4.6 Generalizing the Lemma by Using UNSAT Cores 4.7 Partial Model Generation for Word-Level Reasoning in Bit-Vectors 5 Experimental Evaluations 5.1 Experiment Setup 5.2 The Overall Result 5.3 Effectiveness of SyGuS-APDR in Improving Lemmas 5.4 CHC Solvers Vs. Hardware Model Checkers 6 Related Work 7 Conclusions and Future Work References Synthesis and Repair Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible 1 Introduction 2 Fundamentals 3 Approximation of Essential Bits 4 Flagging Synthesis Problems as Infeasible 4.1 Bit Dependency Shapes 4.2 Tree Upper Bounds 4.3 Bipartite Matching of Variables to Usage Locations 4.4 Infeasibility Checks with Upper Bounds 4.5 Infeasibility Check with the 1 in the Zhegalkin Polynomial 5 Evaluation 5.1 Quality of the Approximations (RQ1) 5.2 Impact of Algorithms 1 and 2 (RQ2) 5.3 Hardness of Flagged Synthesis Problems (RQ3) 5.4 Threats to Validity 6 Related Work 7 Conclusion References Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis 1 Introduction 2 Motivation 3 Overview of Program Repair Using Deductive Synthesis 3.1 Program Verification Using Separation Logic 3.2 Bug Localization 3.3 Template Patch Creation and Constraint Generation 4 Specification Inference 4.1 Inference Rules 4.2 Inference Algorithm 5 Deductive Program Synthesis 5.1 Synthesis Rules 5.2 Synthesis Algorithm 6 Repair Algorithm 7 Evaluation 8 Related Work 9 Limitation and Future Work 10 Conclusion References GPURepair: Automated Repair of GPU Kernels 1 Introduction 2 GPURepair 2.1 GPURepair Architecture and Workflow 2.2 Instrumentation 2.3 Preliminaries 2.4 The Repair Algorithm 3 Related Work 3.1 Comparison with AutoSync 4 Experiments 4.1 Experimental Setup 4.2 Results 5 Conclusion References Applications A Synchronous Effects Logic for Temporal Verification of Pure Esterel 1 Introduction 2 Overview 2.1 Synced Effects 2.2 Forward Verification 2.3 The TRS 3 Language and Specifications 3.1 The Target Language: Pure Esterel 3.2 The Specification Language: Synced Effects 4 Automated Forward Verification 4.1 Forward Rules 4.2 Correctness Checking 5 Temporal Verification via a TRS 5.1 Inference Rules 5.2 Expressiveness of Synced Effects 6 Implementation and Evaluation 6.1 Loops 6.2 Exception Priority 6.3 A Gain on Constructiveness 7 Related Work 7.1 Semantics of Esterel 7.2 Temporal Verification of Esterel 7.3 Synchronous Kleene Algebra (SKA) 8 Conclusion References A Design of GPU-Based Quantitative Model Checking 1 Introduction 2 Linear Temporal Logic for Control 2.1 Discrete Linear Time Invariant System Model 2.2 Syntax and Semantics of LTLC 2.3 Horizon Constraints 2.4 LTLC Model Checking as Feasibility Checking 3 Parallel Model Checker Design 3.1 Preliminary: CUDA 3.2 GPU-Based LTLC Model Checking Algorithm 4 Experiments 5 Analysis 6 Conclusions References Formal Semantics and Verification of Network-Based Biocomputation Circuits 1 Introduction 2 Related Work 3 Formal Semantics 3.1 Discrete Nondeterministic Semantics 3.2 Stochastic Semantics 4 Subset Sum Problem (SSP) 5 Exact Cover (ExCov) 6 Satisfiability (SAT) 7 Experimental Results 7.1 SSP 7.2 ExCov 7.3 SAT 8 Summary References Netter: Probabilistic, Stateful Network Models 1 Introduction 2 Overview 3 The Netter Language 4 Applications 4.1 Warming up 4.2 Traffic Engineering with MPLS 4.3 Stateful Load Balancers 4.4 Defending Against Link-Flooding Attacks 5 Related Work 6 Conclusion and Future Work References Decision Procedures Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories 1 Introduction 2 Preliminaries 3 SCL(T) 4 SCL(T) Decides BS(BD) 5 SCL(T) Extensions and Discussion References Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching 1 Introduction 2 Notation and Basic Definitions 3 Preliminaries 3.1 DPLL(T) 3.2 Congruence Closure 3.3 E-Matching Based Instantiation 4 Finding Conflict and Unit Instances 4.1 Finding Substitutions in the Theory of Equality 4.2 Extension to Linear Arithmetic 5 Implementation and Experiments 6 Related Work 7 Conclusion and Future Work References On Preprocessing for Weighted MaxSAT 1 Introduction 2 Preliminaries 2.1 SAT and MaxSAT 2.2 Boolean Multilevel Optimization (BMO) 3 Generalized Boolean Multilevel Optimization (GBMO) 3.1 GBMO – Definition and Correctness 3.2 Greatest Common Divisor 3.3 Algorithm 4 Trimming the MaxSAT Instance (TrimMaxSAT) 4.1 Algorithm Overview 4.2 SAT-Encoding of the Soft Clause Partitioning 4.3 Candidate List for Partitioning 4.4 Choosing a Candidate for Partition Size m 5 Experimental Results 5.1 Hardware Security Benchmarks 5.2 MaxSAT Evaluation Benchmarks 6 Conclusion and Outlook References Compositional Satisfiability Solving in Separation Logic 1 Introduction 2 Basic Concepts and Motivating Examples 3 Array Separation Logic with Inductive Definitions 4 Regular Unfolding Trees 4.1 Data Structure 4.2 Generating Regular Unfolding Trees 5 Compositional Satisfiability Solver 5.1 Computing Bases 5.2 Decidability and Compositionality 5.3 Compositionality with Small-Model Arithmetic Properties 6 Decidable Fragment SLIDLIA 6.1 Predicate Definition 6.2 Decidability of Fragment AID 7 Implementation and Evaluation 7.1 Efficiency of Compositional Solving 7.2 Experiments on SL-COMP 2019 Benchmarks 8 Related Work 9 Conclusion References Author Index