Static Analysis

Name: Static Analysis | 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings

Sandrine Blazy Thomas Jensen(Herausgeber*in)

Springer (Verlag)

Erschienen am 1. September 2015

XVI, 333 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-662-48288-9 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Preface
Organization
Abstracts of Invited Talks
Static Analysis of x86 ExecutablesUsing Abstract Interpretation
Static Analysis for JavaScript
The SLAYER Static Analyzer
Contents
Static Analysis of Non-interference in Expressive Low-Level Languages
1 Introduction
1.1 Contributions
2 Language and Semantics
2.1 Syntax
2.2 State Space
2.3 Semantics
2.4 Abstraction
3 Non-interference
3.1 Influence
3.2 Program Traces
3.3 Observable Behaviors
3.4 Valid Taints
3.5 Labeled Behaviors
3.6 Similar Stores
3.7 Similar States
3.8 Similar Traces
3.9 Transitivity of Similarity
3.10 Global Transitivity of Similarity
3.11 Labeled Interference in Similar States
3.12 Concrete Termination-Insensitive Labeled Interference
3.13 Abstract Non-interference
4 Discussion
5 Related Work
6 Conclusion
References
Static Analysis with Set-Closure in Secrecy
1 Introduction
2 Background
2.1 Homomorphic Encryption
2.2 The BGV-type Cryptosystem
2.3 Security Model
3 A Basic Construction of a Pointer Analysis in Secrecy
3.1 A Brief Review of a Pointer Analysis
3.2 The Pointer Analysis in Secrecy
4 Improvement of the Pointer Analysis in Secrecy
4.1 Problems of the Basic Approach
4.2 Overview of Improvement
4.3 Level-by-level Analysis
4.4 Ciphertext Packing
4.5 Randomization of Ciphertexts
5 Experimental Result
6 Discussion
A Algorithms
References
A Binary Decision Tree Abstract Domain Functor
1 Introduction
2 Action Path Semantics
3 Branch Condition Path Abstraction
3.1 Branch Condition Graph
3.2 Branch Condition Path Abstraction
4 Binary Decision Tree Abstract Domain Functor
4.1 Definition
4.2 Binary Operations
4.3 Transfer Functions
4.4 Extrapolation Operators
4.5 Other Operators
5 Example
6 Related Work
7 Conclusion
References
Precise Data Flow Analysis in the Presence of Correlated Method Calls
1 Introduction
2 Motivation
2.1 Occurrences of Correlated Calls
2.2 An Example from the Scala Collections Library
3 Background
3.1 Terminology and Notation
3.2 IFDS
3.3 IDE
4 Correlated Calls Analysis
4.1 Transformations from IFDS to IDE
4.2 Converting IDE Results to IFDS Results
4.3 Implementation of Correlated Calls Micro-Functions
4.4 Theoretical Results
4.5 Correlated-Call Receivers
4.6 Efficiency
4.7 Implementation of the Correlated-Calls Analysis
5 Related Work
6 Conclusions
References
May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization
1 Introduction
2 Language
3 An Informal Account of Our Method
4 Must-Have-Finished Analysis
4.1 Definition of MHF
4.2 An Analysis to Infer MHF Sets
5 MHP Analysis
5.1 Local MHP
5.2 Global MHP
6 Conclusions, Implementation and Related Work
References
Shape Analysis for Unstructured Sharing
1 Introduction
2 Overview
3 Inductive Definitions with Set Predicates
4 Composite Memory Abstraction with Set Predicates
5 Static Analysis Algorithms
5.1 Transfer Functions, Local and Non-local Unfolding
5.2 Folding of Inductive Summaries: Inclusion Test, Join and Widening
6 Empirical Evaluation
7 Related Work
8 Conclusion
References
Synthesizing Heap Manipulations via Integer Linear Programming
1 Introduction
2 Preliminaries
2.1 Notations
2.2 Intuition
3 The Algorithm
3.1 Identify the Frames at Each Step
3.2 Infer the Transformation Function
3.3 Infer the Relocation Function
3.4 Infer Selection Logic
3.5 Sequentialization and Dead-Code Elimination
3.6 Constructing the Prologue and Epilogue for the Loop
4 The Integer Linear Programming (ILP) Formulation
4.1 Inferring Transformation and Relocation Functions
4.2 Synthesizing Branch and Loop Conditions
4.3 Synthesizing a Conjunction of Conditions
5 Experimental Results
6 Related Work
7 Conclusions
References
Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR
1 Introduction
2 Iteration Bound Under a Generic Setting
2.1 Preliminaries
2.2 Main Result
3 Iteration Bound for CFG-Represented Programs
3.1 Preliminaries
3.2 Main Result
4 Limitations
5 Conclusion
References
Safety Verification and Refutation by k-Invariants and k-Induction
1 Introduction
2 Algorithm Concepts
2.1 Program Verification as Second Order Logic
2.2 Existing Techniques
2.3 Our Algorithm: kIkI
3 Algorithm Details
3.1 SSA Encoding
3.2 Invariant Inference via Templates
3.3 Guarded Template Domains
3.4 Accelerated Solving of the Problem
4 Implementation
5 Experiments
5.1 kIkI Verifies More Programs Than the Algorithms It Simulates
5.2 kIkI Is at Least as Good as Their Naïve Portfolio
5.3 kIkI Is Comparable with State-of-the-Art Approaches
6 Related Work
7 Conclusions
References
Effective Soundness-Guided Reflection Analysis
1 Introduction
2 Methodology
2.1 Assumptions
2.2 Past Work: Best-Effort Reflection Resolution
2.3 Solar: Soundness-Guided Reflection Resolution
3 Formalism
3.1 The RefJava Language
3.2 Road Map
3.3 Notations
3.4 The SOLAR'S Inference System
3.5 Soundness Criterion
3.6 Identifying Unsoundly Resolved Reflective Calls
3.7 Identifying Imprecisely Resolved Reflective Calls
3.8 Probe
3.9 Static Class Members
4 Evaluation
4.1 Experimental Setup
4.2 Assumptions
4.3 RQ1: Full Automation
4.4 RQ2: Automatically Identifying ``Problematic'' Reflective Calls
4.5 RQ3: Recall and Precision
4.6 RQ4: Efficiency
5 Related Work
6 Conclusion
References
SJS: A Type System for JavaScript with Fixed Object Layout
1 Introduction
2 Design Rationale for the SJS Type System
2.1 Type System for Enforcing Static Object Layout
2.2 Subtyping
3 A Formal Account of the Type System
3.1 Expression
3.2 Types and Qualifiers
3.3 Typing Rules
3.4 Properties of the Type System
4 Summary of Implementation and Evaluation
5 Related Work
References
Refinement Type Inference via Horn Constraint Optimization
1 Introduction
2 Target Language L
3 Refinement Type System for L
3.1 Refinement Type Optimization Problems
4 Applications of Refinement Type Optimization
4.1 Proving Safety
4.2 Disproving Termination
4.3 Proving Termination
4.4 Disproving Safety
5 Horn Constraint Optimization and Reduction from Refinement Type Optimization
5.1 Horn Constraint Optimization Problems
5.2 Reduction from Refinement Type Optimization
6 Horn Constraint Optimization Method
6.1 Sub-Procedure Solve for Solving HCCSs
7 Implementation and Experiments
8 Related Work
9 Conclusion
References
A Simple Abstraction of Arrays and Maps by Program Translation
1 Introduction
2 Example: The Sentinel
3 Galois Connections
3.1 Single Index
3.2 Several Indices, One Per Array
3.3 Dual Indices, Same Array
4 Abstraction of Program Semantics
4.1 Transformation and Correctness
4.2 Precision Loss
4.3 Relative Completeness
5 More Examples
5.1 Matrix Initialization
5.2 Slice Initialization
5.3 Array Copy
5.4 In-Place Array Reversal
5.5 Dutch National Flag
6 Related Work
7 Conclusion and Future Work
References
Property-based Polynomial Invariant Generation Using Sums-of-Squares Optimization
1 Introduction
2 Polynomial Programs and Piecewise Polynomial Discrete-Time Systems
3 Program Invariants as Sublevel Sets
3.1 Collecting Semantics as Postfixpoint Characterization
3.2 Considered Properties: Sublevel Properties P,
3.3 Approach: Compute a P, -Driven Inductive Invariant P
4 SOS Programming for Invariant Generation
5 Benchmarks
5.1 Checking Boundedness of the Set of Variables Values
5.2 Other Properties
6 Templates Bases
7 Related Works and Conclusion
References
Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up Analysis
1 Introduction
2 Informal Overview and Running Example
3 Programming Language
4 Intraprocedural Connection Analysis
5 Interprocedural Connection Analysis
5.1 Abstract Domain
5.2 Interprocedural Top-Down Connection Analysis
5.3 Bottom Up Compositional Connection Analysis
6 Implementation and Experimental Evaluation
7 Related Work, Discussion and Conclusions
References
Parallel Cost Analysis of Distributed Systems
1 Introduction
2 The Model of Distributed Programs
2.1 Syntax
2.2 Semantics
3 Parallel Cost of Distributed Systems
4 Block-Level Cost Analysis of Serial Execution
5 Parallel Cost Analysis
5.1 Distributed Flow Graph
5.2 Inference of Parallel Cost
6 Parallel Cost Analysis with Cooperative Concurrency
7 Experimental Evaluation
8 Conclusions and Related Work
References
A Forward Analysis for Recurrent Sets
1 Introduction
2 Background
2.1 Concrete Semantics
2.2 Recurrent Sets in the Abstract
3 Finding a Universal Recurrent Set
3.1 Idea of the Algorithm
3.2 Abstract State Graph
3.3 The Algorithm
4 Examples
5 Experiments
6 Related Work
7 Conclusion and Future Work
References
Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration
1 Introduction
2 Preliminaries
2.1 Model Syntax
2.2 Model Semantics
2.3 Abstract Acceleration
2.4 Support Functions
3 Abstract Acceleration with Inputs
3.1 Overview of the Algorithm
3.2 Abstract Acceleration Without Guards
3.3 Computation of Abstract Matrices
3.4 Abstract Acceleration with Guards: Estimation of the Number of Iterations
3.5 Abstract Matrices for Complex Eigenvalues
4 Case Study
5 Implementation and Experimental Results
6 Conclusions and Future Work
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken