Static Analysis
18th International Symposium, SAS 2011. Venice, Italy, September 14-16, 2011. Proceedings
Erschienen am 15. September 2011
XII, 387 Seiten
978-3-642-23702-7 (ISBN)
Beschreibung
This book constitutes the refereed proceedings of the 18th International Symposium on Static Analysis, SAS 2011, held in Venice, Italy, in September 2011.
The 22 revised full papers were selected from 67 submissions. Also included in this volume are the abstracts of the invited talks that were given at the symposium by renowned experts in the field. The papers address all aspects of static analysis, including abstract domains, abstract interpretation, abstract testing, data flow analysis, bug detection, program transformation, program verification, security analysis and type checking.
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
