Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1,

This open access two-volume set constitutes the proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, which was held during March 27 – April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The total of 41 full papers presented in the proceedings was carefully reviewed and selected from 141 submissions. The volume also contains 7 tool papers; 6 Tool Demo papers, 9 SV-Comp Competition Papers. The papers are organized in topical sections as follows: Part I: Game Theory; SMT Verification; Probabilities; Timed Systems; Neural Networks; Analysis of Network Communication. Part II: Verification Techniques (not SMT); Case Studies; Proof Generation/Validation; Tool Papers; Tool Demo Papers; SV-Comp Tool Competition Papers. ETAPS Foreword Preface Organization Contents – Part II Contents – Part I Verification Techniques (not SMT) Directed Reachability for Infinite-State Systems 1 Introduction 2 Preliminaries 3 Directed Search Algorithms 4 Directed Reachability 4.1 Distance Under-approximations 4.2 From Petri Net Relaxations to Distance Under-approximations 4.3 Directed Reachability Based on Distance Under-approximations 5 Experimental Results References Bridging Arrays and ADTs in Recursive Proofs 1 Introduction 2 Preliminaries 3 Synthesis of Recursive Relational Invariants 3.1 Overview 3.2 Classifying Operations 4 Recipe 1: Linear Scan 4.1 Motivating Example 4.2 Algorithm Description 5 Recipe 2: Noop-based synthesis 5.1 Motivating Example 5.2 Algorithm details 6 Evaluation 7 Related Work 8 Conclusion and Outlook References A Two-Phase Approach forConditional Floating-Point Verification 1 Introduction 2 A Two-Phase Approach 2.1 First Phase: Whole Program Analysis 2.2 Second Phase: Numerical Kernel Analysis 2.3 Soundness Guarantees 3 First Phase: Whole Program Analysis 4 Second Phase: Static Analysis with Daisy and CBMC 5 State of the Art on Real-World Programs 6 Evaluation of our Two-Phase Approach 7 Related Work 8 Conclusion Acknowledgements References Symbolic Coloured SCC Decomposition 1 Introduction 1.1 Related Work 2 Problem Definition 2.1 Graphs and Strongly Connected Components 2.2 Coloured SCC Decomposition Problem 3 Algorithm 3.1 Symbolic Computation Model 3.2 Forward-backward Algorithm 3.3 Lock-step Algorithm 3.4 Coloured Lock-step Algorithm 3.5 Correctness and Complexity of the Coloured Lock-step Algorithm 4 Experimental Evaluation 4.1 Implementation 4.2 Experiments 5 Conclusions References Case Studies Local Search with a SAT Oracle for Combinatorial Optimization 1 Introduction 2 Background 2.1 Constraint Optimization Program (COP) 2.2 The Cell Placement Problem 2.2.1 Constraint Optimization Program for Cell Placement 2.3 Solving COP with SAT 2.3.1 Bit-vector Solving and SAT. 2.3.2 Extending Bit-vector Solving to Optimization. 2.4 Local Search Algorithms 2.4.1 Basic Local Search Strategy. 2.4.2 Neighbourhood Functions. 2.4.3 Advanced Versions of Local Search 3 Local Search with SAT Oracle (LSSO) 4 LSSO Algorithms for the Cell Placement Problem 4.1 Neighbourhood Generators 4.1.1 Neighbourhood Generator 4.1.2 N2: a Family of Neighbourhood Generators 4.1.3 Hill-climbing Neighbourhood Generator N3. 4.2 LSSO-based Algorithms for Placement 5 Experimental Results 6 Conclusion References Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities 1 Introduction 1.1 Proof of Concept 1.2 Detecting Intra-update Sniping Vulnerabilities 2 A Model for Infrastructure as Code 2.1 CloudFormation Infrastructures 2.2 Model of a CloudFormation Infrastructure 2.3 Execution Semantics 2.4 Upgrade Semantics and Security Policy 3 Architectural Design of the Hayha Tool 3.1 Upgrade States 3.2 Splitting Dependencies 3.3 Finding Vulnerabilities 4 Experiments 5 Related Work 6 Conclusion Acknowledgement References Proof Generation/Validation Certifying Proofs in the First-Order Theory of Rewriting 1 Introduction 2 Preliminaries 3 Formulas 4 Certificates 5 FORTify 6 FORT-h 7 Experiments 8 Conclusion References Syntax-Guided Quantifier Instantiation 1 Introduction 2 Background 3 SyGuS Quantifier Instantiation (SyQI) 3.1 Grammar Construction 3.2 Implementation Details 4 Experiments 5 Conclusion References Making Theory Reasoning Simpler 1 Introduction 2 Preliminaries and Related Work 3 Gaussian variable elimination 4 Arithmetic subterm generalization 5 Evaluation 6 Cancellation 7 Experimental evaluation 8 Conclusion References Deductive Stability Proofs for Ordinary Differential Equations 1 Introduction 2 Background: Di erential Dynamic Logic 3 Asymptotic Stability of an Equilibrium Point 3.1 Mathematical Preliminaries 3.2 Formal Specification 3.3 Lyapunov Functions 3.4 Asymptotic Stability Variations 4 General Stability 4.1 General Stability and General Attractivity 4.2 Specialization 5 Stability in KeYmaera X 6 Related Work 7 Conclusion References Tool Papers An SMT-Based Approach for Verifying Binarized Neural Networks 1 Introduction 2 Background 3 Extending Reluplex to Support Sign Constraints 4 Optimizations 5 Implementation 6 Evaluation 7 Related Work 8 Conclusion Acknowledgements. References cake_lpr: Verified Propagation Redundancy Checking in CakeML 1 Introduction 2 Background 2.1 HOL4 and CakeML 2.2 SAT Problems and Clausal Proofs 3 Linear Propagation Redundancy 4 CakeML Proof Checking 4.1 Verification Strategy 4.2 Verified Optimizations 5 Benchmarks 5.1 SaDiCaL PR Benchmarks 5.2 SAT Race 2019 Benchmarks 5.3 Mutilated Chessboard RAT Microbenchmarks 6 Related Work 7 Conclusion Acknowledgments. A Correctness Theorem for cake_lpr References Deductive Verification of Floating-Point Java Programs in KeY 1 Introduction 2 Background 2.1 Introduction to KeY 2.2 Floating-Point Arithmetic in Java 3 Floating-Point Support in KeY 3.1 Arithmetics 3.2 Transcendental Functions 4 Evaluation 4.1 Benchmark Programs 4.2 Proof Obligation Generation 4.3 Evaluation of SMT Floating-Point Support 4.4 Evaluation of Support for Transcendental Functions in KeY 4.5 Discussion and insights 5 Related Work 6 Conclusion Acknowledgements References Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types 1 Introduction 2 Overview of Helmholtz and Michelson 2.1 Helmholtz 2.2 An Example Contract in Michelson 2.3 Specification 3 Refinement Type System for Mini-Michelson 3.1 Operational Semantics 3.2 Refinement Type System 4 Tool Implementation 4.1 Annotations 4.2 Case Study: Contract with Signature Verification 4.3 Experiments 5 Related Work 6 Conclusion References SyReNN: A Tool for Analyzing Deep Neural Networks 1 Introduction 2 Preliminaries 3 A Symbolic Representation of DNNs 4 Computing the Symbolic Representation 4.1 Algorithm for Extend 4.2 Representing Polytopes 5 SyReNN tool 6 Applications of SyReNN 6.1 Integrated Gradients 6.2 Visualization of DNN Decision Boundaries 6.3 Patching of DNNs 7 Related Work 8 Conclusion and Future Work References MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers 1 Introduction 2 Background 2.1 A Brief Overview of Algorithm Selection 2.2 Supervised Learning, Adaptive Boosting, Curse of Dimensionality, and K-Fold Cross-Validation 2.3 Unsupervised Learning and Principal Component Analysis 3 An overview of MachSMT 3.1 Features, Preprocessing, and Learning 3.2 Variants of MachSMT 3.3 Using MachSMT 3.4 User-defined Features 4 Experimental Evaluation of MachSMT on SMT-COMP 2019 and 2020 Data 4.1 Experimental Setup and Methodology 4.2 Experimental Results 5 Analysis and Discussion of Results 6 Related Work 6.1 Key di erences between SATZilla and MachSMT 6.2 Algorithm Selection for Logic Solvers and Their Applications 7 Conclusions and Future Work References dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts 1 Introduction 2 Decision tree learning for controller representation 3 Tool 4 Predicate domain 4.1 Categorical predicates 4.2 Algebraic predicates 5 Predicate selection 6 New insights about determinization 7 Experiments 8 Conclusion References Tool Demo Papers HLola: a Very Functional Tool for Extensible Stream Runtime Verification 1 Introduction 2 The HLola Tool 3 Example Specifications References AMulet 2.0 for Verifying Multiplier Circuits 1 Introduction 2 Circuit Verification using Computer Algebra 3 Usage 4 AMulet 2.0 5 Evaluation 6 Conclusion References RTLola on Board: Testing Real Driving Emissions on your Phone 1 Introduction 2 RDE Monitoring on Android 3 User Experience 4 Conclusion References Replicating Restart with ProlongedRetrials: An Experimental Report 1 Introduction 2 Restart with Prolonged Retrials 3 Experiments 4 Conclusion References A Web Interface for Petri Nets with Transits and Petri Games 1 Introduction 2 Web Interface for Petri Nets with Transits 3 Web Interface for Petri Games 4 Implementation Details 5 Conclusion References Momba: JANI Meets Python 1 Introduction 2 Scenario-Based Model Construction 3 Validation by Simulation 4 Harvesting the Benefits 5 Conclusion References SV-Comp Tool Competition Papers Software Verification: 10th Comparative Evaluation (SV-COMP 2021) 1 Introduction 2 Organization, Definitions, Formats, and Rules 3 Reproducibility 4 Results and Discussion 5 Conclusion References CPALockator: Thread-Modular Analysis with Projections 1 Verification Approach 2 Software Architecture 3 Strengths and Weaknesses 4 Tool Setup and Configuration 5 Project and Contributors References Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution) 1 Overview 2 Leveraging Compiler Optimizations 3 The Price of Precision 4 Evaluation Acknowledgement: References Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution) 1 Verification Approach and Software Architecture 2 Strengths and Weaknesses 3 Tool Setup and Configuration 4 Software Project References Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints 1 Verification Approach 2 Software Architecture 3 Strengths and Weaknesses 4 Tool Setup and Configuration 5 Software Project and Contributors References Towards String Support in JayHorn (Competition Contribution) 1 The JayHorn Approach and Architecture 2 Encoding of String Operations 2.1 The CompareTo Operation 2.2 Integer to String conversion 2.3 StartsWith and EndsWith 2.4 CharAt 3 Performance of the String Encoding 4 Tool Setup 5 Software Project and Contributors References JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution) 1 Overview 2 Tool Improvements for SV-COMP 2021 3 Strengths and Weaknesses 4 Tool Setup 5 Software Project References Symbiotic 8: Beyond Symbolic Execution 1 Verification Approach 2 Software Architecture 3 Strengths and Weaknesses 4 Tool Setup and Project Contributors 5 Software Project and Contributors References VeriAbs: A Tool for Scalable Verification by Abstraction (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 Author Index