Static Analysis

Name: Static Analysis | 18th International Symposium, SAS 2011. Venice, Italy, September 14-16, 2011. Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

18th International Symposium, SAS 2011. Venice, Italy, September 14-16, 2011. Proceedings

Eran Yahav(Herausgeber*in)

Springer (Verlag)

Erschienen am 15. September 2011

XII, 387 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-23702-7 (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

Title
Preface
Conference Organization
Table of Contents
Widening and Interpolation
Program Analysis and Machine Learning: A Win-Win Deal
References
Program Analysis for Web Security
Astr´ee: Design and Experience
Formal Model Reduction
References
Purity Analysis: An Abstract Interpretation Formulation
Introduction
The Language, Concrete Semantics, and the Problem
The WSR Analysis as an Abstract Interpretation
Transformer Graphs: An Informal Overview
The Abstract Domain
The Abstract Semantics
Optimizations
Empirical Evaluation
Related Work
References
The Complexity of Abduction for Separated Heap Abstractions
Introduction
Preliminaries
Syntax of Separated Heap Abstractions
Semantics
Separated Abduction Problems
Membership in NP
NP-completeness
From 3-SAT to the Abduction Problem (P1)
From the Abduction Problem (P1) to 3-SAT
NP-completeness and PTIME Results for Fragments
SAP() is NP-complete
rSAP() Is in PTIME
Conclusion
References
Efficient Decision Procedures for Heaps Using STRAND
Introduction
Data-Structures, Submodels, Elasticity and Strand
An Overview of Strand
Recursively Defined Data-Structures
Submodels
Elasticity and Strand
The New Decision Procedure for Strand
Comparison with Earlier Known Decision Procedure
Experiments
Related Work
Conclusions
References
The Flow-Insensitive Precision of Andersen's Analysis in Practice
Introduction
Flow-Insensitive Imprecision in Andersen's Analysis
Precise Analysis via Witness Search
A Precise Algorithm for Finite Memory
Handling Summarized Locations
A Symbolic Encoding
Is There a Precision Gap in Practice?
Discussion: Why Is There No Precision Gap in Practice?
Threats to Validity
Related Work
Conclusion
References
Side-Effect Analysis of Assembly Code
Introduction
The Concrete Semantics
Analysis of Side-Effects
Effect Integration
Effect Computation
Correctness
Experimental Results
Conclusion
References
Directed Symbolic Execution
Introduction
Directed Symbolic Execution
Forward Symbolic Execution
Shortest-Distance Symbolic Execution
Call-Chain-Backward Symbolic Execution
Mixing CCBSE with Forward Search
Experiments
Synthetic Programs
GNU Coreutils
Threats to Validity
Other Related Work
Conclusion
References
Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation
Introduction
Background and Problem Definition
Background: Compositional Symbolic Execution
Problem Definition: Must Summary Checking
Phase 1: Static Change Impact Analysis
Phase 2: Predicate-Sensitive Change Impact Analysis
Phase 3: Must Summary Validity Checking
Dealing with Partial Summaries
Recomputing Invalidated Summaries
Experimental Results
Implementation
Benchmarks
Results
Related Work
Conclusions
References
On Sequentializing Concurrent Programs
Introduction
Concurrent Programs
Compositional Semantics
Bounded Semantics
Global-Round Explorations
Context-Bounding
Delay-Bounding
Context-Bounding vs. Delay-Bounding
Related Work
Conclusion
References
Verifying Fence Elimination Optimisations
Introduction
The x86-TSO Memory Model and CompCertTSO
The Optimisations
Formalisation of Traces and Simulations
Proofs of the Optimisations
Coq Experience
Related Work
Conclusion
References
An Efficient Static Trace Simplification Technique for Debugging Concurrent Programs
Introduction
Preliminaries
Concurrent Program Execution Model
General Trace Simplification Problem
SimTrace: Efficient Static Trace Simplification
Modeling of the Dependence Relation
A Theorem of Trace Equivalence
SimTrace Algorithm
Implementation and Experiments
Related Work
Conclusion
References
A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs
Higher-Order Is Hard
Concurrency Makes It Harder
Challenges to Reasoning about Higher-Order Concurrency
P(CEK)S: An Abstract Machine Model of Concurrent, Higher-Order Computation
P(CEK)S: A Concrete State-Space
P(CEK)S: A Factored Transition Relation
A Shift in Perspective
Concurrent Transition in the P(CEK)S Machine
A Systematic Abstract Interpretation of P(CEK)S
Running the Analysis
A Fixed Point Interpretation
Termination
Concurrent Abstract Transitions
Soundness
Extracting Flow Information
Extracting MHP Information
MHP: Making Strong Transitions with Singleton Threads
Strategies for Abstract Thread id Allocation
Advantages for MHP Analysis
Flow Analysis of Concurrent Higher-Order Programs
Complexity
Related Work
Limitations and Future Work
References
Abstract Domains of Affine Relations
Introduction
Terminology and Notation
Relating AG and KS Elements
Relating KS and MOS
MOS and KS are Incomparable
Converting MOS Elements to KS
Converting KS without Pre-State Guards to MOS
Converting KS with Pre-State Guards to MOS
Symbolic Implementation of the Function for MOS
Using KS for Interprocedural Analysis
Experiments
Related Work
References
Transitive Closures of AÆne Integer Tuple Relations and Their Overapproximations
Introduction
Background
Related Work
Powers and Transitive Closures
Introduction
Single Disjunct
Multiple Disjuncts
Properties
Strongly Connected Components
Implementation Details
Experiments
Type Size Inference
Equivalence Checking
Iteration Space Slicing
Conclusions and Future Work
References
Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs
Introduction
Analysis of Logico-Numerical Programs
Abstract Interpretation
Abstract Acceleration
Classical Application of Abstract Acceleration
Logico-Numerical Abstract Acceleration
Motivations for Our Approach
Decoupling Numerical and Boolean Transition Functions
Decoupling Accelerable from Non-accelerable and Boolean Transition Functions
Using Inputization Techniques
Partitioning Techniques for Logico-Numerical Acceleration
Experimental Evaluation
Conclusion and Related Work
References
Invisible Invariants and Abstract Interpretation
Introduction
Fixed Point Computation Strategy
Invisible Invariants
Engineering Invisible Invariants
Experiments
Fixed Point Strategies
Computing the Abstract Transformer
Benchmarks
Related Work
Conclusion
References
An Abstraction-Refinement Framework for Trigger Querying
Introduction
Preliminaries
Trigger Querying
Predicate Abstraction
Relating Concrete and Abstract Languages
Approximating Triggers
Refinement
Between the over and under Approximations
The Refinement Algorithm
Variants of Trigger Querying
Query Checking
Constrained Trigger Querying
Necessary Conditions
Discussion
References
Bound Analysis of Imperative Programs with the Size-Change Abstraction
Introduction
Examples
Program Model and Size-Change Abstraction
Order Constraints
Size-Change Abstraction (SCA)
Main Steps of our Analysis
Computing Transition Systems
Disjunctiveness in Algorithm 1
Pathwise Analysis in Algorithm 1
Bound Computation
Contextualization
Bound Algorithm
Heuristics for Extracting Norms
Related Work
Experiments
References
Satisfiability Modulo Recursive Programs
Introduction
Examples
Our Satisfiability Procedure
Properties of Our Procedure
The Leon Verification System
Experimental Evaluation
Related Work
References
Probabilistically Accurate Program Transformations
Introduction
Loop Perforation
Computational Patterns
Modeling and Analysis
Contributions
Example
Preliminaries
Patterns and Analyses
Sum Pattern
Mean Pattern
Argmin-Sum Pattern
Ratio Pattern
Discussion
Related Work
Conclusion
References
Probabilistic Abstractions with Arbitrary Domains
Introduction
An Example
Constructing a Valid Abstraction
Stochastic 2-Player Games
Abstractions of Probabilistic Programs
Abstracting NPPs
An Algorithm for Constructing Valid Abstractions
Refining Abstractions: Quantitative Widening Delay
Experiments
Conclusions
References
Software Verification Using k-Induction
Introduction
Overview
Control Flow Graphs and Loops
Proof Rule and Verification Algorithm
Graphical Description of k-induction Proof Rule
Formal Definition of k-induction Proof Rule
Theoretical Properties of the k-induction Rule
Experimental Evaluation
Related Work and Conclusions
References
Using Bounded Model Checking to Focus Fixpoint Iterations
Introduction
Background and Notations in Abstract Interpretation
Our Method
Reduced Transition Multigraph and Path Focusing
Finding Focus Paths
Algorithm
Correctness and Termination
Self-Loops
Extensions
Narrowing
Acceleration
Partitioning
Input-Output Relations
Implementation and Preliminary Results
Related Work
Conclusion and Future Work
References
Author Index

Inhalt (PDF)

Systemvoraussetzungen

Als PDF speichern Als Link merken