Static Analysis

Name: Static Analysis | 17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010, Proceedings

Radhia Cousot Matthieu Martel(Herausgeber*in)

Springer (Verlag)

Erschienen am 13. September 2010

XI, 473 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-15769-1 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken