Static Analysis: 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, ProceedingsChris Hankin, Igor Siveroni Static analysis allows us to determine aspects of the dynamic behavior of p- grams and systems without actually executing them. Traditionally used in - timizing compilers, static analysis is now also used extensively in veri'cation, software certi'cation and semantics-based manipulation. The research com- nity in static analysis covers a broad spectrum from foundational issues - new semantic models of programming languages and systems - through to practical tools.TheseriesofStatic AnalysisSymposia hasservedasthe primaryvenue for presentation and discussion of theoretical, practical and application advances in the area. This volume contains the papers accepted for presentation at the 12th Int- national Static Analysis Symposium (SAS 2005) which was held 7-9 September 2005 at Imperial College London. A total of 66 papers were submitted; the Program Committee held an online discussion which led to the selection of 22 papers for presentation. The selection was based on scienti'c quality, originality and relevance to the scope of SAS. Every paper was reviewed by at least 3 PC members or external referees. This volume also includes abstracts of talks given by the two invited speakers: Samson Abramsky FRS (University of Oxford) and Andrew Gordon (Microsoft Research, Cambridge). OnbehalfoftheProgramCommittee, theProgramChairwouldliketothank all of the authors who submitted papers and all of the external referees for their careful work in the reviewing process. The Program Chair would also parti- larly like to thank Igor Siveroni who provided local support for the conference management system and who helped in organizing the structure of this volume. |
Contents
Invited Talks | 1 |
Generation of Basic Semialgebraic Invariants Using Convex Polyhedra | 19 |
Inference of WellTypings for Logic Programs with Application | 35 |
Memory Space Conscious Loop Iteration Duplication for Reliable | 52 |
Memory Usage Verification for OO Programs | 70 |
Abstraction Refinement for Termination | 87 |
A Game Semantic Approach | 102 |
LocalityBased Abstractions | 118 |
Taming False Alarms from a DomainUnaware C Analyzer by | 203 |
A Scalable ConstraintBased Analysis Toolkit | 218 |
A Generic Framework for Interprocedural Analysis of Numerical | 235 |
Finding Basic Block and Variable Correspondence | 251 |
Boolean Heaps | 268 |
Interprocedural Shape Analysis for CutpointFree Programs | 284 |
Understanding the Origin of Alarms in Astrée | 303 |
PairSharing Analysis of ObjectOriented Programs | 320 |
TypeSafe Optimisation of Plugin Architectures | 135 |
Using Dependent Types to Certify the Safety of Assembly Code | 155 |
The PER Model of Abstract Noninterference | 171 |
A Relational Abstraction for Functions | 186 |
Exploiting Sparsity in Polyhedral Analysis | 336 |
Secure Information Flow as a Safety Problem | 352 |
Other editions - View all
Static Analysis: 12th International Symposium, SAS 2005, London, UK ... Chris Hankin,Igor Siveroni No preview available - 2005 |
Common terms and phrases
abstract domain alarms algorithm allows analysis application approach approximation array assignment assume block bound closure compiler complete Computer concrete condition consider constraint construction contains correspondence defined definition denote dependent described duplication elements equality equivalence example execution exists expression extended false field Figure finite flow formal function given graph heap implementation inequalities inference initial input interpretation invariants Italy iteration language linear LNCS logic loop means memory method Note objects observe obtained operator original pointer polynomial precision predicates present problem procedure properties prove reachable reduced references refinement relation represented respectively rules safety secure semantics sequence share space static structures technique termination Theorem transformation transition true variables vector