Static Analysis: 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021, Proceedings (Lecture Notes in Computer Science)

Preface
Organization
Invited Talks
Oracle Parfait: The Flavour of Real-World Vulnerability Detection and Intelligent Configuration
Interactive Code Analysis
Pointer Analysis of Bytecode Programs for Effective Formal Verification of Smart Contracts
Contents
Fast and Efficient Bit-Level Precision Tuning
	1 Introduction
	2 Running Example
	3 Generation of Constraints for Bit-Level Tuning
		3.1 Preliminary Notations and Definitions
		3.2 Integer Linear Problem Formulation
		3.3 Policy Iteration for Optimized Carry Bit Propagation
	4 Correctness
		4.1 Soundness of the Constraint System
		4.2 ILP Nature of the Problem
	5 Experimental Results
	6 Conclusion and Perspectives
	A  Appendix
	References
Hash Consed Points-To Sets
	1 Introduction
	2 Background and Motivation
		2.1 Background
		2.2 Motivating Examples
	3 Approach
		3.1 Hash Consed Points-To Sets
		3.2 Exploiting Set Properties
	4 Evaluation
		4.1 Implementation and Experimental Setup
		4.2 Results and Discussion
	5 Related Work
	6 Conclusion
	References
Backward Symbolic Execution with Loop Folding
	1 Introduction
	2 Preliminaries
	3 Backward Symbolic Execution and k-Induction
		3.1 Backward Symbolic Execution (BSE)
		3.2 k-Induction
		3.3 Equivalence of BSE and k-Induction
	4 BSE with Loop Folding (BSELF)
		4.1 The BSELF Algorithm
		4.2 The Computation of the Initial Invariant Candidate
		4.3 Overapproximation of an Inductive Set
		4.4 Optimizations
		4.5 Examples
	5 Experimental Evaluation
		5.1 Comparison of BSELF and BSE
		5.2 Comparison of BSELF to State-of-the-Art Tools
	6 Related Work
	7 Conclusion
	References
Accelerating Program Analyses in Datalog by Merging Library Facts
	1 Introduction
	2 Overview
		2.1 Accelerating by Domain-Wise Merging
		2.2 Learning a Merging over Library Code
	3 Preliminary
	4 Constructing Domain-Wise Merging in Datalog
		4.1 1-Domain-Wise Merging
		4.2 N-Domain-Wise Merging
		4.3 Properties of Mergings
	5 Algorithm
		5.1 Learn Merging Heuristics of Library Facts from Input Programs
		5.2 Finding a Maximal Merging
	6 Implementation and Evaluation
		6.1 Points-to Analysis
		6.2 Liveness Analysis
	7 Related Work
	8 Conclusion
	A Incremental Merging in N-Domain-Wise Cases
	B Proof: The Monotonicity of Mergings
	C Detailed Performance of 4DM in Points-to Analysis on Large Projects
	D Detailed Performance of 4DM in Liveness Analysis
	References
Static Analysis of Endian Portability by Abstract Interpretation
	1 Introduction
	2 Syntax and Concrete Semantics
		2.1 Syntax
		2.2 Semantics of Low-Level Simple C Programs
		2.3 Semantics of Double Programs
		2.4 Properties of Interest
	3 Memory Abstraction
		3.1 Cells
		3.2 Shared Bi-Cells
		3.3 Cell Synthesis
		3.4 Abstract Join
		3.5 Semantics of Simple Statements
		3.6 Semantics of Double Statements
	4 Value Abstraction
	5 Evaluation
		5.1 Idiomatic Examples
		5.2 Open Source Benchmarks
		5.3 Industrial Case Study
	6 Conclusion
	References
Verified Functional Programming of an Abstract Interpreter
	1 Introduction
	2 IMP: A Small Imperative Language
	3 Operational Semantics
	4 Abstract Domains
	5 An Example of Abstract Domain: Intervals
		5.1 Forward Binary Operations on Intervals
		5.2 Backward Operators
	6 Specialized Abstract Domains
		6.1 Numerical Abstract Domains
		6.2 Memory Abstract Domains
	7 A Weakly-Relational Abstract Memory
	8 Statement Abstract Interpretation
	9 Conclusion and Further Works
	References
Disjunctive Interval Analysis
	1 Introduction
	2 Range Decision Diagrams
	3 Implementing Boxes with RDDs
		3.1 Lattice Operations
		3.2 Variable Hoisting
		3.3 Arithmetic Operators
		3.4 Widening
	4 Experimental Evaluation
		4.1 Experimental Setup
		4.2 Performance
		4.3 Precision
	5 Related Work
	6 Conclusion
	References
Static Analysis of ReLU Neural Networks with Tropical Polyhedra
	1 Introduction and Related Work
	2 Preliminaries and Notations
		2.1 Zones
		2.2 Tropical Polyhedra
		2.3 From Zone to Tropical Polyhedra and Vice-Versa
		2.4 Feedforward ReLU Networks
	3 Abstraction of Linear Maps
		3.1 Zone-Based Abstraction
		3.2 Octagon Abstractions and (max, +, -) Algebra
	4 Validation of Multi-layered Neural Networks
	5 Implementation, Experiments and Benchmarks
	6 Conclusion and Future Work
	References
Exploiting Verified Neural Networks via Floating Point Numerical Error
	1 Introduction
	2 Background and Related Work
	3 Problem Definition
	4 Exploiting a Complete Verifier
	5 Exploiting an Incomplete Verifier
	6 Discussion
	7 Conclusion
	References
Verifying Low-Dimensional Input Neural Networks via Input Quantization
	1 Introduction
	2 Method
	3 Experiments
		3.1 Experimental Setup
		3.2 Experimental Results
	4 Conclusion
	References
Data Abstraction: A General Framework to Handle Program Verification of Data Structures
	1 Introduction
	2 Preliminaries: Horn Clauses
		2.1 Solving Programs with Assertions Using Horn Clauses
		2.2 Horn Clauses and Horn Problems
		2.3 Horn Problem Induced by an Abstraction
		2.4 Horn Clauses Transformations
	3 Data Abstraction: Abstracting Horn Clauses
		3.1 Implementing Horn Clauses Abstraction
		3.2 Combining Data Abstractions
	4 Data Abstraction: Quantifier Removal
		4.1 A Quantifier Elimination Technique Parametrized by insts
		4.2 Constructing a Good Heuristic insts
	5 Cell Abstraction: A Complete Data Abstraction
		5.1 Cell Abstractions
		5.2 Instantiating Cell Abstractions
	6 Implementation and Experiments
		6.1 The Full Algorithm
		6.2 Experimental Setting and Results
		6.3 Analysis
	7 Related Work
	8 Conclusion
	References
Toward Neural-Network-Guided Program Synthesis and Verification
	1 Introduction
	2 Predicate Synthesis from Positive/Negative Examples
		2.1 The Problem Definition and Our Method
		2.2 Experiments
		2.3 Extensions for Non-linear Constraints
	3 Predicate Synthesis from Implication Constraints and Its Application to CHC Solving
		3.1 The Extended Synthesis Problem and Our Method
		3.2 Preliminary Experiments
	4 Related Work
	5 Conclusion
	A  Additional Information for Sect.2
		A.1  On Three-Layer vs Four-Layer NNs
		A.2  On Activation Functions
		A.3  On Biases
	B  Additional Information for Sect.3
	References
Selective Context-Sensitivity for k-CFA with CFL-Reachability
	1 Introduction
	2 Challenges
		2.1 k-CFA
		2.2 Selective Context-Sensitivity
	3 Preliminary
		3.1 CFL-Reachability Formulation of K-CFA-based Pointer Analysis
		3.2 Transitivity of LC-Path Concatenation
	4 CFL-Reachability-based Selective Context-Sensitivity
		4.1 Necessity for Context-Sensitivity
		4.2 Selectx: A Context-Sensitivity Selection Algorithm
		4.3 Precision Loss
		4.4 Time and Space Complexities
	5 Evaluation
		5.1 kcs vs. s-kcs
		5.2 Z-kcs vs. s-kcs
	6 Related Work
	7 Conclusion
	References
Selectively-Amortized Resource Bounding
	1 Introduction
	2 Overview
		2.1 Decomposing Resource Updates to Selectively Amortize
		2.2 Finding a Selective-Amortization Decomposition
	3 Decomposing Resource Usage
		3.1 Selective Amortization by Decomposition
		3.2 Soundness of Group and Segment Decomposition
	4 Selecting a Decomposition
	5 Empirical Evaluation
	6 Related Work
	7 Conclusion
	References
Reduced Products of Abstract Domains for Fairness Certification of Neural Networks
	1 Introduction
	2 Tool Architecture
		2.1 Tool Input
		2.2 Front-End
		2.3 Analysis Engine
		2.4 Abstract Domains
		2.5 Tool Output
	3 Experimental Evaluation
		3.1 Effect of Neural Network Structure on Precision and Scalability
		3.2 Precision-vs-Scalability Tradeoff
		3.3 Leveraging Multiple CPUs
	4 Conclusion and Future Work
	References
A Multilanguage Static Analysis of Python Programs with Native C Extensions
	1 Introduction
	2 An Extension Module Example
	3 Concrete Semantics
	4 Abstract Semantics
	5 Experimental Evaluation
	6 Related Work
	7 Conclusion
	References
Automated Verification of the Parallel Bellman–Ford Algorithm
	1 Introduction
	2 Background
		2.1 The Bellman–Ford Algorithm
		2.2 The VerCors Verifier
	3 Approach
	4 Proof Mechanization
	5 Evaluation and Discussion
	6 Related Work
	7 Conclusion
	References
Improving Thread-Modular Abstract Interpretation
	1 Introduction
	2 Side-Effecting Systems of Constraints
	3 A Local Trace Semantics
		3.1 Thread Creation
		3.2 Locking and Unlocking
		3.3 Local and Global Variables
		3.4 Completeness of the Local Constraint System
		3.5 Example Formalism for Local Traces
	4 Static Analysis of Concurrent Programs
		4.1 Protection-Based Reading
		4.2 Lock-Centered Reading
		4.3 Write-Centered Reading
	5 Experimental Evaluation
	6 Conclusion
	References
Thread-Modular Analysis of Release-Acquire Concurrency
	1 Introduction
	2 Related Work
	3 Overview
		3.1 Thread Modular Analysis with Partial Order Domain
		3.2 Over-Approximating PO Domain
	4 Preliminaries
	5 Concrete Semantics
		5.1 Modification Orders as Posets
	6 Abstract Semantics
		6.1 Mo Posets as Lattices
		6.2 Abstract Semantics of RA Programs
		6.3 Abstracting the Abstraction: Approximating Mo Posets
		6.4 Posets as a Generic Abstraction
	7 Thread-Modular Abstract Interpretation
		7.1 Analysis Algorithms
		7.2 A Note on Precision
		7.3 Loops and Termination
	8 Implementation and Evaluation
		8.1 Implementation
		8.2 Summary of Benchmarks
		8.3 Observations
	9 Conclusions
	References
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
	1 Introduction
	2 Preliminaries
		2.1 FOL with List
	3 Symbolic Automatic Relations
		3.1 Symbolic Synchronous Automata
		3.2 Symbolic Automatic Relations
		3.3 Expressing Predicates on Lists
		3.4 An Application to ICE-Learning-Based CHC Solving with Lists
	4 Undecidability Result
	5 Reduction to CHC Solving
		5.1 Overview
		5.2 Translation
		5.3 Correctness
	6 Experiments
	7 Related Work
	8 Conclusion
	References
Compositional Verification of Smart Contracts Through Communication Abstraction
	1 Introduction
	2 Background
	3 MicroSol: Syntax and Semantics
	4 Participation Topology
	5 Local Reasoning in Smart Contracts
		5.1 Guarded Properties and Split Invariants
		5.2 Localizing a Smart Contract Bundle
	6 Implementation and Evaluation
	7 Related Work
	8 Conclusions
	References
Automatic Synthesis of Data-Flow Analyzers
	1 Introduction
	2 Motivation
	3 Approach
		3.1 Problem Definition
		3.2 Syntax-Guided Synthesis
		3.3 Abstraction-Guided Search Space Pruning
		3.4 Brevity-Guided Search Space Pruning
		3.5 The DFASy Synthesis Algorithm
	4 Evaluation
		4.1 Implementation
		4.2 Dataset
		4.3 Baselines
		4.4 Results and Analysis
		4.5 Case Study: Null Pointer Detection
		4.6 Discussions
	5 Related Work
		5.1 Synthesis by Examples
		5.2 Synthesis by Templates
		5.3 Data-Flow Analysis
		5.4 Synthesis of Static Analysis Rules
	6 Conclusion
	References
Author Index