Static Analysis: 27th International Symposium, SAS 2020, Virtual Event, November 18–20, 2020, Proceedings

Description

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