Static Analysis
17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010, Proceedings
Published on 13. September 2010
XI, 473 pages
978-3-642-15769-1 (ISBN)
Description
More details
Other editions
Additional editions
Radhia Cousot | Matthieu Martel
Static Analysis
17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010, Proceedings
Book
09/2010
1st Edition
Springer
€53.49
Shipment within 5-7 days
Content
- Title Page
- Preface
- Organization
- Table of Contents
- Time of Time
- Static Verification for Code Contracts
- Code Contracts
- Verification Steps
- Heap Abstraction
- Abstract Interpretation Fixpoints
- Weakest Precondition Analysis
- Conclusion
- References
- Translation Validation of Loop Optimizations and Software Pipelining in the TVOC Framework
- Introduction
- Validating Global Optimizations in TVOC
- Validating Loop Optimizations
- Validating Software Pipelining
- A Gentle Introduction to Software Pipelining
- Validating a Software Pipeline
- Future Work: Validating Pipelining That Uses Hardware Support
- Conclusion
- References
- Size-Change Termination and Transition Invariants
- Introduction
- Size-Change Termination (SCT)
- A Running Example
- Some Size-Change Definitions
- Composition of Size-Change Graphs
- A Closure Algorithm to Decide the SCT Property
- Transition Invariants (TI)
- Programs Defined by Transitions
- Termination by Transition Invariants
- Transition Predicate Abstraction (TPA)
- Correctness Proofs and Abstractions
- From Graphs to Transition Relations
- SCT and Disjunctive Well-Foundedness
- Size-Change Graphs and Transition Predicate Abstraction
- Decision Problems for Termination Analyses
- Transformer on Abstract Relations
- Composition of Abstract Relations
- Special Case: Associative Composition of Abstract Relations
- Discussion: Qualitative Differences
- References
- Using Static Analysis in Space: Why Doing so?
- Introduction
- Static Analysis and the European Standards for Space
- Principles of the ECSS
- Static Analysis for Validation
- Static Analysis for Verification
- Static Analysis for ISVV
- Static Analysis for V&V of Reuse Software and Regression Testing
- Conclusion on Static Analysis and Standards
- Impact of Static Analysis on the Development Strategy
- Link between Static Analysis and Development Strategy
- Static Analysis and Programming Language
- Static Analysis and Model Driven Engineering
- Conclusion on the Impact of Static Analysis on the Development Strategy
- Static Analysis at Astrium Space Transportation
- Type Checking
- Abstract Interpretation
- Model Checking
- Theorem Proving
- Conclusion
- References
- Statically Inferring Complex Heap, Array, and Numeric Invariants
- Introduction
- Deskcheck Architecture
- Modeling of Programs
- Base Domains
- Combining Domains
- Domain Operations
- Partial Order
- Join and Widening
- Assignment
- Examples
- Linked Lists
- Arrays
- Numeric Predicates
- Reference Counting
- Experiments
- Related Work
- References
- From Object Fields to Local Variables: A Practical Approach to Field-Sensitive Analysis
- Introduction
- Motivation: Field-Sensitive Termination Analysis
- A Simple Imperative Bytecode
- Preliminaries: Inference of Constant Access Paths
- Locality Conditions for Numeric and Reference Fields
- Polyvariant Transformation of Fields to Local Variables
- Experiments
- Conclusions and Related Work
- References
- Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
- Introduction and Motivation
- Notations and Definitions
- Integer Interpreted Automata
- Termination and Ranking Functions
- Illustrating Example
- Computing Affine Ranking Functions
- A Greedy Polynomial-Time Procedure
- Completeness
- Worst-Case Computational Complexity (WCCC)
- Implementation and Experimental Results
- Related Work
- Conclusion
- Contributions
- FutureWork
- References
- Deriving Numerical Abstract Domains via Principal Component Analysis
- Introduction
- Notations
- The Parallelotope Domains
- Abstract Operations on Parallelotopes
- Union and Intersection
- Assignment
- Test
- On the Implementation of Abstract Operators
- Principal Component Analysis
- Orthogonal Simple Component Analysis
- Implementation
- Optimizing the Parallelotope Domains
- Experimental Evaluation
- Related Work
- Conclusions and Future Work
- References
- Concurrent Separation Logic for Pipelined Parallelization
- Introduction
- Parallelizing Transformations
- Parallelizing a Program
- CSL with Asynchronous Channels
- Channel Endpoint Histories
- Predicate Logic
- Resource Invariants
- Instructions
- Hoare Logic
- Parallelized Program with Proof
- Model and Operational Semantics
- The Separation Algebra of Resources
- Predicate Formulae
- Operational Semantics
- Soundness
- Related Work
- Future Work and Conclusion
- References
- Automatic Abstraction for Intervals Using Boolean Formulae
- Introduction
- The Drive for Automatic Abstraction
- Specifying Extreme Values with Universal Quantifiers
- Finessing Universal Quantifiers with Boolean Formulae
- Worked Examples
- Deriving a Transfer Function for a Block
- Deriving a Transfer Function for an Operation with Many Modes
- Deriving a Transfer Function for a Block with Many Modes
- Abstracting Boolean Formulae
- Abstracting Boolean Formulae with Octagonal Inequalities
- Abstracting Boolean Formulae with Affine Equalities
- Applying Action Systems of Guarded Updates
- Related Work
- Concluding Discussion
- References
- Interval Slopes as a Numerical Abstract Domain for Floating-Point Variables
- Introduction
- Background
- Floating-Point Arithmetic
- Interval Arithmetic
- Floating-Point Slopes
- Floating-Point Version of Interval Slopes
- Semantics of Arithmetic Operations
- Order Structure
- Analysis of Floating-Point Programs
- Case Studies
- Related Work
- Conclusion
- References
- A Shape Analysis for Non-linear Data Structures
- Introduction
- Semantic Settings
- Concrete Semantics
- Symbolic Heaps and Intermediate Semantics
- Abstract Semantics: The Analysis
- Relevance of Variables and Abstraction
- Quantified Variables and Termination
- Managing Graphs
- Experimental Results
- Conclusions
- References
- Modelling Metamorphism by Abstract Interpretation
- Introduction
- Background
- Modelling Metamorphism
- Abstracting Metamorphism
- Widening Phases for Regular Metamorphism
- Related Works and Discussion
- References
- Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
- Introduction
- Preliminaries
- Simplified Form
- Algorithm to Compute Simplified Forms
- Basic Algorithm
- Making Simplification Practical
- Integration with Program Analysis
- Experimental Results
- Impact of On-Line Simplification on Analysis Scalability
- Redundancy in Program Analysis Constraints
- Complexity of Simplification in Practice
- Related Work
- References
- Compositional Bitvector Analysis for Concurrent Programs with Nested Locks
- Introduction
- Preliminaries
- Locking Information
- Bitvector Data Flow Analysis
- Concurrent Data Flow Framework
- Normal Runs
- TheAnalysis
- A Case Study
- Application and Future Work
- References
- Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely
- Introduction
- Basics
- Solving Systems of Order-Concave Equations
- Systems of SDP-Equations
- Quadratic Zones and Relaxed Abstract Semantics
- Experimental Results
- Conclusion
- References
- {\sc Boxes}: A Symbolic Abstract Domain of Boxes
- Introduction
- Linear Decision Diagrams
- The {\sc Boxes} Abstract Domain
- Widening
- {\sc Boxes} and Finite Powerset of {\sc Box}
- Experiments
- Conclusion
- References
- Alternation for Termination
- Introduction
- Overview
- Preliminaries
- Termination Certificates
- Proving Non-termination
- Algorithm
- Sub-procedures Called by TREX
- Handling Nested Loops, Function Calls and Pointers
- Limitations of TREX
- Experiments
- Micro-benchmarks
- Windows Drivers
- Related Work
- Conclusion
- References
- Interprocedural Analysis with Lazy Propagation
- Introduction
- A Basic Analysis Framework
- Analysis Instances
- Derived Lattices
- Computing the Solution
- An Abstract Data Type for Transfer Functions
- Problems with the Basic Analysis Framework
- Extending the Framework with Lazy Propagation
- Modifications of the Analysis Lattice
- Modifications of the Abstract Data Type Operations
- Recovering Unknown Field Values
- Implementation and Experiments
- Related Work
- Conclusion
- References
- Verifying a Local Generic Solver in Coq
- Introduction
- The Local Generic Solver RLD
- Systems of Constraints
- Strategy Trees
- Solutions
- Functional Implementation with Explicit State Passing
- Proof of Theorem 4
- Instrumentation
- Implementation in Coq
- Invariants
- Putting Things Together
- Conclusion
- References
- Thread-Modular Counterexample-Guided Abstraction Refinement
- Introduction
- Illustration
- Preliminaries
- Algorithm
- Abstract Reachability Analysis
- Checking Counterexample for Spuriousness
- Refine: Extract New Exception Set
- Applying TM-CEGAR to Peterson's Protocol
- Parallel Mutex Loop
- Polynomial Runtime
- Experiments
- Related Work
- Conclusion
- References
- Generating Invariants for Non-linear Hybrid Systems by Linear Algebraic Methods
- Introduction
- Algebraic Hybrid Systems and Inductive Assertions
- New Continuous Consecution Conditions
- Handling Non-linear Differential Systems
- Obtaining Optimal Degree Bounds
- Examples and Experimental Results
- Handling Algebraic Discrete Transition Systems
- Discrete Transition with Polynomial Systems
- Discrete Transition with Fractional Systems
- Conclusions
- References
- Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods
- Introduction
- Overall Summary of the Approach
- Probabilistic Programs
- Probabilistic Program Annotations
- The Special Case of Loops
- Constraint-Solving for Quantitative Annotations
- Linear Probabilistic Programs and Parametrised Annotations
- Constructing Machine-Solvable Constraints
- Solving Constraints and Heuristics
- Soundness and Completeness
- Three Examples
- Example One: Binomial Update
- Example Two: Generating a Biased Coin from a Fair One
- Example Three: Uniform Distribution
- Nested Loops
- Alternative Automated Methods
- Aims and Conclusions
- References
- Abstract Interpreters for Free
- Introduction: Can We Get Two for the Price of One?
- An Example to Illustrate Correspondence and Redundancy
- The Two-Step Method: Snipping and Trickling
- Continuation-Passing-Style ?-Calculus
- ANa\"{ı}ve Attempt: "Throw Hats on Everything"
- Step 1: Snipping the Knots with Store-Passing Style
- Making a Snip
- Option 1: Snipping $Env Clo$
- Option 2: Snipping $Clo Env$
- Optional Snips
- Step 2: Trickling Up Abstraction
- Abstracting the Leaves of the State-Space Dependence Graph
- Recursively Constructing the Abstract State-Space
- Galois Inference Rules
- Synthesizing an Abstract Interpretation for CPS (Option 1)
- Synthesizing an Abstract Interpretation for CPS (Option 2)
- Flow-Sensitivity, Field-Sensitivity and Context-Sensitivity
- Related Work
- Summary and Conclusion
- References
- Points-to Analysis as a System of Linear Equations
- Introduction
- Points-toAnalysis
- A First-Cut Approach
- The Modified Approach
- The Algorithm
- Context-Sensitive Analysis
- Soundness and Precision
- Experimental Evaluation
- Related Work
- Conclusion
- References
- Strictness Meets Data Flow
- Introduction
- Type-and-Effect System
- Type-and-Effect Inference System
- Principality
- Connection to Traditional Type Inference
- Effect System Soundness
- Inference Algorithm
- Properties
- Optimisations
- Standard Strictness Analysis and Optimisations
- Inlining to Expose Standard Strictness Optimisation
- Absent Argument Optimisation
- Implicational Strictness
- Transformation Soundness
- Related Work
- Conclusion and Future Work
- References
- Automatic Verification of Determinism for Structured Parallel Programs
- Introduction
- Overview
- Motivating Example
- Establishing Determinism by Independence
- Reporting Potential Sources of Non-determinism
- Concrete Semantics
- Determinism
- Pairwise Semantics
- Abstract Semantics
- Abstract State
- Implementation
- Reference Arrays
- Evaluation
- Results
- Summary
- Related Work
- Conclusion
- References
- Author Index
