Static Analysis: 19th International Symposium, SAS 2012, Deauville, France, September 11-13, 2012. Proceedings

Description

This book constitutes the thoroughly refereed proceedings of the 19th International Symposium on Static Analysis, SAS 2012, held in Deauville, France, in September 2012. The 25 revised full papers presented together with 4 invited talks were selected from 62 submissions. The papers address all aspects of static analysis, including abstract domains, abstract interpretation, abstract testing, bug detection, data flow analysis, model checking, new applications, program transformation, program verification, security analysis, theoretical frameworks, and type checking. Front Matter....Pages - Computer-Aided Cryptographic Proofs....Pages 1-2 A Voyage to the Deep-Heap....Pages 3-3 Semantics and Analyses for JavaScript and the Web....Pages 4-4 Efficient May Happen in Parallel Analysis for Async-Finish Parallelism....Pages 5-23 Modular Static Analysis with Zonotopes....Pages 24-40 Polyhedral Analysis Using Parametric Objectives....Pages 41-57 Inference of Polynomial Invariants for Imperative Programs: A Farewell to Gröbner Bases....Pages 58-74 A New Abstract Domain for the Representation of Mathematically Equivalent Expressions....Pages 75-93 An Abstract Domain to Infer Types over Zones in Spreadsheets....Pages 94-110 Bilateral Algorithms for Symbolic Abstraction....Pages 111-128 Making Abstract Interpretation Incomplete: Modeling the Potency of Obfuscation....Pages 129-145 Invariant Generation for Parametrized Systems Using Self-reflection....Pages 146-163 Automatic Fence Insertion in Integer Programs via Predicate Abstraction....Pages 164-180 Control Flow Analysis for the Join Calculus....Pages 181-197 When the Decreasing Sequence Fails....Pages 198-213 Loop Leaping with Closures....Pages 214-230 Path-Sensitive Backward Slicing....Pages 231-247 Symbolic Learning of Component Interfaces....Pages 248-264 Liveness-Based Pointer Analysis....Pages 265-282 Succinct Representations for Abstract Interpretation....Pages 283-299 Craig Interpretation....Pages 300-316 Satisfiability Solvers Are Static Analysers....Pages 317-333 A Generalization of Stålmarck’s Method....Pages 334-351 A Structural Soundness Proof for Shivers’s Escape Technique....Pages 352-369 Modular Heap Analysis for Higher-Order Programs....Pages 370-387 Binary Reachability Analysis of Higher Order Functional Programs....Pages 388-404 On the Limits of the Classical Approach to Cost Analysis....Pages 405-421 Termination Proofs for Linear Simple Loops....Pages 422-438 Finding Non-terminating Executions in Distributed Asynchronous Programs....Pages 439-455 Back Matter....Pages -