Static Analysis: 27th International Symposium, SAS 2020, Virtual Event, November 18–20, 2020, Proceedings (Lecture Notes in Computer Science Book 12389)

This book constitutes the refereed proceedings of the 27th International Symposium on Static Analysis, SAS 2020, held in Chicago, IL, USA, in November 2020. The 14 regular papers presented in this book together with 2 invited talks and 1 extended abstract, were carefully reviewed and selected from 34 submissions. The papers cover topics such as abstract domains; abstract interpretation; automated deduction; data flow analysis; debugging; deductive methods; emerging applications; model-checking; program transformations; predicate abstraction; security analysis; tool environments and architectures; and type checking. Due to the Corona pandemic this event was held virtually. Preface 0 Organization 0 Polynomial Invariants for Affine Programs (Invited Talk) 0 Contents 0 Invited Talks 0 Static Resource Analysis at Scale (Extended Abstract) 0 1 Introduction 0 2 Static Complexity Analysis with Infer 0 3 Diff-Time Deployment at Scale 0 References 71 Cost Analysis of Smart Contracts Via Parametric Resource Analysis 0 1 Introduction 0 2 The Parametric Resource Analysis Approach 0 3 Translating into the CHC IR 0 4 Defining Resources and Cost Models 0 5 Performing the Resource Analysis 0 6 Some Experimental Results 0 7 Related Work 0 8 Conclusions and Future Work 0 A Brief Description of Selected Michelson Contracts 0 References 0 Regular Papers 0 Memory-Efficient Fixpoint Computation 46 1 Introduction 46 2 Fixpoint Computation Preliminaries 49 2.1 Bourdoncle's Recursive Iteration Strategy 50 2.2 Memory Management During Fixpoint Computation 51 2.3 Problem Statement 52 3 Declarative Specification of Optimal Memory Configuration blueMredopt 53 3.1 Declarative Specification of blueDpostredopt 54 3.2 Declarative Specification of blueAchkredopt 56 3.3 Declarative Specification of blueDpostredopt 56 3.4 Declarative Specification of blueDpreredopt 57 4 Efficient Algorithm to Compute blueMredopt 58 5 Implementation 59 6 Experimental Evaluation 60 6.1 Task T1: Verifying User-Provided Assertions 61 6.2 Task T2: Proving Absence of Buffer Overflows 62 7 Related Work 64 8 Conclusion 65 A Proofs 66 A.1 Nesting forest (V, maroonN) and total order (V, PineGreen) in Sect. 3 66 A.2 Optimality of blueMredopt in Sect. 3 67 A.3 Correctness and efficiency of GenerateFMProgram in Sect. 4 70 References 71 Abstract Neural Networks 0 1 Introduction 0 2 Motivation 0 2.1 Merging Nodes 0 3 Preliminaries 0 3.1 Deep Neural Networks 0 3.2 Common Activation Functions 0 4 Abstract Neural Networks 0 5 Layer-Wise Abstraction Algorithm 0 5.1 Computability 0 5.2 Walkthrough Example 0 6 Layer-Wise Abstraction: Instantiations and Examples 0 6.1 Interval Hull Domain with ReLU Activation Functions 0 6.2 Interval Hull Domain with Leaky ReLUs 0 6.3 Interval Hull Abstraction with Non-continuous Functions 0 6.4 Powerset Abstraction, ReLU, and red"0362redbin 0 7 Proof of Sufficient Conditions 0 7.1 Vector Representatives 0 7.2 Proof of Soundness Theorem 0 8 Related Work 0 9 Conclusion and Future Directions 0 References 0 Termination of Polynomial Loops 0 1 Introduction 0 2 Preliminaries 0 3 Transformation to Triangular Weakly Non-linear Form 0 3.1 Transforming Loops 0 3.2 Finding Automorphisms to Transform Loops into twn-Form 0 4 Computing Closed Forms 0 5 Reducing Termination of tnn-Loops to `3́9`42`"̇613A``45`47`"603ATh(S, RA) 0 6 Complexity Analysis 0 7 Related Work and Conclusion 0 References 0 Stratified Guarded First-Order Transition Systems 0 1 Introduction 0 2 Basic Definitions 0 3 Stratification and Guardedness 0 4 Universal So Quantifier Elimination 0 5 Stratified Guarded Updates 0 6 Allowing Guarded Stratified Resets 0 7 Conclusion 0 References 0 Predicate Abstraction and CEGAR for HFLZ Validity Checking 0 1 Introduction 0 2 Preliminaries: Higher-Order Fixed-Point Logic HFLZ 0 3 Predicate Abstraction 0 4 Counterexample-Guided Abstraction Refinement 0 4.1 Counterexample 0 4.2 Feasibility Check 0 4.3 Predicate Discovery and Abstraction Refinement 0 5 Implementation and Evaluation 0 6 Related Work 0 7 Conclusion 0 References 0 Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis 0 1 Introduction 0 2 Overview 0 3 Problem Definition 0 4 Algorithm 0 4.1 Simulation 0 4.2 Candidate Invariant Conjecture 0 4.3 Reducing the Noise 0 4.4 Checking a Candidate Invariant 0 4.5 Generalizing from Counterexamples 0 4.6 Floating-Point Invariant 0 4.7 Implementation 0 5 Experimental Evaluation 0 5.1 State-of-the-Art Techniques 0 5.2 Experimental Setup 0 5.3 Comparison with State-of-the-Art 0 5.4 Efficiency 0 5.5 Parameter Sensitivity 0 6 Related Work 0 7 Conclusion 0 References 0 Formal Framework for Reasoning About the Precision of Dynamic Analysis 0 1 Introduction 0 2 Preliminaries 0 3 Topological Characterisation of the Precision of Dynamic Analysis 0 3.1 Modelling Dynamic Program Analysis 0 3.2 Harming Dynamic Analysis 0 4 Model Validation 0 4.1 Control Flow Analysis 0 4.2 Code Coverage 0 4.3 Harming Dynamic Data Analysis 0 5 Related Works 0 6 Discussion and Future Works 0 References 0 Simple and Efficient Computation of Minimal Weak Control Closure 0 1 Introduction 0 2 Background 0 3 Program Slicing Using WCC and SCC 0 4 Efficient Computation of Minimal WCC 0 4.1 An Informal Account of Our Approach 0 4.2 An Overapproximation of the Weakly Deciding Vertices 0 4.3 Generating Minimal Weakly Deciding Vertices 0 4.4 Computing Minimal WCC 0 4.5 Worst-Case Time Complexity 0 5 Experimental Evaluation 0 6 Related Work 0 7 Conclusion and Future Work 0 A Appendix 0 References 0 A Library Modeling Language for the Static Analysis of C Programs 0 1 Introduction 0 2 Syntax and Concrete Semantics 0 2.1 Syntax 0 2.2 Environments 0 2.3 Evaluation 0 2.4 Relational Semantics 0 3 Generic Abstract Semantics 0 3.1 Abstract Domain 0 3.2 Evaluations 0 3.3 Transfer Functions 0 4 Specific Abstract Semantics: The Case of C Strings 0 5 Experiments 0 5.1 Juliet 0 5.2 Coreutils 0 6 Conclusion 0 A Stub Examples 0 A.1 Predicates 0 A.2 Memory Management 0 A.3 File Descriptors 0 A.4 Command-Line Arguments 0 References 0 Interprocedural Shape Analysis Using Separation Logic-Based Transformer Summaries 0 1 Introduction 0 2 Overview 0 3 Abstraction of Sets of States and State Transformations 0 4 Procedure Summarization 0 5 Intraprocedural Analysis 0 6 Abstract Composition 0 7 Interprocedural Analysis Based on Function Summaries 0 7.1 Analysis of a Call Site Using an Existing Summary 0 7.2 Inference of a New Context Summary 0 8 Experimental Evaluation 0 9 Related Works and Conclusion 0 A Raw Experimental Data 0 References 0 Probabilistic Lipschitz Analysis of Neural Networks 0 1 Introduction 0 2 Language Definition 0 2.1 Language Syntax 0 2.2 Language Semantics 0 3 Lipschitz Analysis 0 3.1 Instrumented cat Semantics 0 3.2 Jacobian Analysis 0 3.3 Box Analysis 0 4 Algorithms 0 4.1 PROLIP Algorithmic Primitive 0 4.2 Sketch of Proof-Search Algorithm 0 4.3 Discussion 0 5 Empirical Evaluation 0 5.1 Experimental Setup 0 5.2 Results 0 6 Related Work 0 7 Conclusion 0 A Proof of Lemma 3 0 B Proof of Corollary 4 0 C Proof of Theorem 6 0 D Proof of Corollary 8 0 E Proof of Theorem 11 0 F Translating Neural Networks into pcat 0 G Details of Box Analysis 0 References 0 On Multi-language Abstraction 0 1 Introduction 0 2 The Multi-language Framework 0 2.1 Order-Sorted Algebras 0 2.2 Multi-languages and Their Algebras 0 3 Algebraic Perspective on Collecting Semantics 0 3.1 Fixpoint Calculation of Collecting Semantics 0 4 Basic Notions of Algebraic Abstract Semantics 0 5 The Multi-language Abstraction 0 5.1 Combining Abstractions of Different Languages 0 6 Related Works 0 7 Discussion and Concluding Remarks 0 A Concrete and Abstract Semantics of Imp and Num 0 References 0 Exact and Linear-Time Gas-Cost Analysis 0 1 Introduction 0 2 Overview of Gas Analysis 0 2.1 Exact Bound Analysis and Runtime Overhead 0 2.2 Handling Unbounded Computation 0 3 Formal Analysis 0 3.1 A Simplistic Programming Language 0 3.2 Static Gas Analysis 0 3.3 Soundness of Analysis 0 4 Implementation and Evaluation 0 4.1 Evaluation 0 5 Related Work 0 6 Conclusion 0 References 0 Farkas-Based Tree Interpolation 0 1 Introduction 0 2 Background 0 2.1 Linear Systems 0 3 Tree Interpolation for Linear Real Arithmetic 0 3.1 Proper Labeling 0 3.2 Tree Interpolation Property in Farkas Interpolation Algorithm 0 3.3 A Tree Interpolation Algorithm Based on Decomposing Farkas Interpolation 0 4 Negative Results for the Algorithms for Flexible, Dual Farkas and Dual Decomposed Interpolation 0 5 Experimental Evaluation 0 6 Conclusion 0 A Appendix A 0 References 0 Author Index 0