Tools and Algorithms for the Construction and Analysis of Systems: 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 Dublin, Ireland, April 25–30, 2020, Proceedings 2

This open access two-volume set constitutes the proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, which took place in Dublin, Ireland, in April 2020, and was held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020. The total of 60 regular papers presented in these volumes was carefully reviewed and selected from 155 submissions. The papers are organized in topical sections as follows: Part I: Program verification; SAT and SMT; Timed and Dynamical Systems; Verifying Concurrent Systems; Probabilistic Systems; Model Checking and Reachability; and Timed and Probabilistic Systems. Part II: Bisimulation; Verification and Efficiency; Logic and Proof; Tools and Case Studies; Games and Automata; and SV-COMP 2020. ETAPS Foreword Preface Organization Contents – Part II Contents – Part I Bisimulation An O(m log n) algorithm for branching bisimilarity on labelled transition systems 1 Introduction 2 Branching bisimilarity 3 The algorithm 3.1 High-level description of the algorithm 3.2 Abstract algorithm 3.3 Correctness 3.4 In-depth description of the algorithm 3.5 Time complexity 4 Splitting blocks 5 Experimental evaluation References Verifying Quantum Communication Protocols with Ground Bisimulation* 1 Introduction 2 Quantum CCS 3 Algorithm 4 Implementation and Experiments 4.1 Implementation 4.2 BB84 Quantum Key Distribution Protocol 4.3 Experimental Results 5 Conclusion and Future Work Appendix References Deciding the bisimilarity of context-free session types 1 Introduction 2 Context-free session types 3 An algorithm to decide type bisimilarity 4 Correctness of the algorithm 5 Evaluation 6 Conclusion References Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities 1 Introduction 2 Processes, Compositions, and Reductions 3 Temporal Logics 4 Sharp Bisimilarity 5 LTS Reduction 6 Experimentation 7 Related Work 8 Conclusion References Verification and Efficiency How Many Bits Does it Take to Quantize Your Neural Network? 1 Introduction 2 Quantization of Feed-forward Networks 3 Robustness is Non-monotonic in the Number of Bits 4 Verification of Quantized Networks using Bit-precise SMT-solving 5 Experimental Results 5.1 Scalability and performance 5.2 Comparison to other methods 5.3 The effect of quantization on robustness 5.4 Network specifications beyond robustness 6 Conclusion Acknowledgments References Highly Automated Formal Proofs over Memory Usage of Assembly Code 1 Introduction 2 Formal Memory Usage Certificates 3 FMUC Verification 3.1 Verification Tools Used 3.2 Per-block Verification 3.3 Verification of Function Body 3.4 Composition 4 Case Study: Xen Project 5 Related Work 6 Conclusion References GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts 1 Introduction and Main Applications 2 Gas Analysis using Gasol 3 Gas Optimization using Gasol 4 Related Tools and Conclusions References CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering 1 Introduction 2 Intel Running Average Power Limit (RAPL) 3 CPU Energy Meter 4 Applications 5 Conclusion References Logic and Proof Practical Machine-Checked Formalization of Change Impact Analysis 1 Introduction 2 Background 2.1 Change Impact Analysis 2.2 Regression Test Selection and Regression Proof Selection 2.3 Build Systems 2.4 The Coq Proof Assistant and Mathematical Components 3 Formal Model 3.1 Definitions 3.2 Example 3.3 Correctness Approach 4 Model Encoding 4.1 Encoding in Coq 4.2 Correctness Statements 5 Component Hierarchies 5.1 Formal Model of Hierarchies 5.2 Encoding and Correctness in Coq 6 Tool Implementation 6.1 Optimizations 6.2 Encapsulation 7 Evaluation of the Model 7.1 Tool Integration 7.2 Projects 7.3 Experimental Setup 7.4 Results 8 Related Work 9 Conclusion Acknowledgments References What’s Decidable About Program Verification Modulo Axioms? 1 Introduction 2 Illustrative Example 3 Preliminaries 3.1 Program Syntax 3.2 Executions and Semantics of Uninterpreted Programs 3.3 Feasibility of Executions Modulo Axioms 3.4 Program Verification Modulo Axioms 4 Coherence Modulo Axioms 4.1 Terms Computed and Assumptions Accumulated by Executions 4.2 Coherence 5 Axioms over Relations 5.1 Verification modulo EPR axioms 5.2 Reflexivity, Irreflexivity, and Symmetry 5.3 Transitivity 5.4 Strict Partial Orders 5.5 Strict Total Orders 6 Axioms Over Functions 6.1 Associativity 6.2 Commutativity 6.3 Idempotence 7 Combining Axioms 8 Related Work 9 Conclusions References Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting 1 Introduction 2 Preliminaries 3 Infinity Predicate 4 Executable Infinity Predicate 5 Normal Form Predicate 6 Conclusion and Future Work References Fold/Unfold Transformations for Fixpoint Logic 1 Introduction 2 First-Order Fixpoint Logic MuArith 2.1 Syntax 2.2 Semantics 2.3 Program Verification as Validity Checking of MuArith Formulas 2.4 Auxiliary Definitions 3 Fold/Unfold-Like Transformations 3.1 Overview of Transformations for MuArith 3.2 Transformations for μ-Formulas 3.3 Fold/Unfold for ν-Formulas 4 Further Examples 4.1 Relational Reasoning on Recursive Programs 4.2 Proving Temporal Properties 5 Algorithm and Evaluation 5.1 Algorithm 5.2 Implementation and Experiments 6 Related Work 7 Conclusions References Tools and Case Studies Verifying OpenJDK’s LinkedList using KeY 1 Introduction 2 LinkedList in OpenJDK 2.1 Integer overflow bug 2.2 Reproduction 3 Specification and verification of BoundedLinkedList 3.1 Specification 3.2 Verification 4 Discussion 4.1 Related work Self-references References Analysing installation scenarios of Debian packages 1 Introduction 2 Overview of the case study and analysis methodology 2.1 Debian packages 2.2 Managing package installation 2.3 Principles and workflow of the analysis method 2.4 Presentation of results 3 Design and implementation of the tool chain 3.1 Front-end 3.2 Feature trees and constraints 3.3 Specifications of UNIX commands 3.4 Analysis by symbolic execution 3.5 Scenarios 4 Results and impact 4.1 Coverage of the case study 4.2 Corpus mining 4.3 Bugs found 4.4 Lessons learnt 5 Conclusion References Endicheck: Dynamic Analysis for Detecting Endianness Bugs 1 Introduction 2 Dynamic Analysis for Checking Endianness 2.1 Algorithm Overview 2.2 Shadow Memory 2.3 Propagation of Metadata 2.4 Discussion: Analysis Design and Precision 3 Implementation 4 User Guide 5 Evaluation 5.1 Case Study 5.2 Search for Bugs 5.3 Performance 5.4 Discussion 6 Related Work 7 Conclusion 7.1 FutureWork Acknowledgments References Describing and Simulating Concurrent Quantum Systems 1 Processes 1.1 A programming language 1.2 Symbolic quantum calculation 1.3 No cloning 1.4 Other notable features 2 Straightforward description 3 Performance on examples 4 Conclusions 5 Data Availability and Acknowledgements References EMTST: Engineering the Meta-theory of Session Types 1 Introduction 2 EMTST: a Tool for Representing the Meta-theory of Session Types 2.1 Environments and Multiple Name Scopes 3 Two Case Studies on Binary Session Types 3.1 The Original System 3.2 The Revised System 4 Related Work and Conclusions Acknowledgements Bibliography Games and Automata Solving Mean-Payo Games via Quasi Dominions 1 Introduction 2 Mean-Payo Games 3 Solving Mean-Payo Games via Progress Measures 4 Solving Mean-Payo Games via Quasi Dominions 5 Experimental Evaluation 6 Concluding Remarks References Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems 1 Introduction 2 Preliminaries 3 Partial-Order Reduction 3.1 Weak Stubborn Sets 3.2 Correctness 3.3 Optimising D2w 4 Parameterised Boolean Equation Systems 5 PBES Solving Using POR 6 Experiments 7 Conclusion References Polynomial Identification of w-Automata! 1 Introduction 2 Preliminaries 3 Negative Results 4 Outline for the positive results 5 The characteristic sample for the automaton 6 Learning the automaton 7 Characteristic sample for a DPA 7.1 Constructing the canonical forest of a DPA 7.2 Constructing the characteristic sample for a DPA 8 The learning algorithm for a DPA 9 The sample T_Acc and the learning algorithm for a DMA 10 Discussion References Part 6 SV-COMP 2020 Advances in Automatic Software Verification: SV-COMP 2020 1 Introduction 2 Organization, Definitions, Formats, and Rules 3 Reproducibility 4 Results and Discussion 5 Conclusion References 2LS: Heap Analysis and Memory Safety (Competition Contribution) 1 Overview 2 New Features 2.1 Combinations of Abstract Domains 2.2 Symbolic Paths 2.3 Re-using Freed Memory Object for Next Allocations 2.4 Generic Abstract Domain Templates 3 Strengths and Weaknesses 4 Tool Setup 5 Software Project References COASTAL: Combining Concolic and Fuzzing for Java (Competition Contribution) 1 Verification Approach and Software Architecture 1.1 Strategies 1.2 Observers and Models 2 Strengths and weaknesses 3 Tool setup 4 Software Project References Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution) 1 Overview and Software Architecture 2 Strengths and Weaknesses 3 Tool Setup and Configuration 4 Software Project and Contributors References VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution) 1 Verification Approach 1.1 Tool Enhancements 2 Software Architecture 3 Strengths and Weaknesses 4 Tool Setup and Configuration 5 Software Project and Contributors References GACAL: Conjecture-based Verification (Competition Contribution) 1 Verification Approach 2 Tool Setup and Software Project and Architecture 3 Evaluation 4 Conclusions and Future Work References Java Ranger at SV-COMP 2020 (Competition Contribution) 1 Approach 2 Architecture 3 Strengths And Weaknesses 4 Tool Setup and Configuration 5 Software Project and Contributors 6 Acknowledgments References JDart: Dynamic Symbolic Execution for Java Bytecode (Competition Contribution) 1 Overview 2 Architecture 3 Strengths and Weaknesses 4 Tool Setup 5 Software Project References Map2Check: Using Symbolic Execution and Fuzzing (Competition Contribution) 1 Overview 2 Verification Approach 3 Software Architecture 4 Strengths andWeaknesses of the Approach 5 Tool Setup and Configuration 6 Software Project References PredatorHP Revamped (Not Only) for Interval-Sized Memory Regions and Memory Reallocation (Competition Contribution) 1 Verification Approach and Software Architecture 1.1 The Predator Shape Analyzer 1.2 Recent Modifications of PredatorHP 2 Strengths and Weaknesses 3 Contributors, Software Project, and the Tool Setup References Symbiotic 7: Integration of Predator and More (Competition Contribution) 1 Verification Approach 2 Software Architecture 3 Strengths and Weaknesses 4 Tool Setup and Configuration 5 Software Project and Contributors References Ultimate Taipan with Symbolic Interpretation and Fluid Abstractions (Competition Contribution) 1 Verification Approach 2 Strengths and Weaknesses 3 Architecture, Setup, Configuration, and Project References Author Index