Invited Papers.- Refactoring Using Type Constraints.- Programming Language Design and Analysis Motivated by Hardware Evolution.- Contributed Papers.- A Compilation Model for Aspect-Oriented Polymorphically Typed Functional Languages.- Lattice Automata: A Representation for Languages on Infinite Alphabets, and Some Applications to Verification.- Compositional Verification and 3-Valued Abstractions Join Forces.- Formalised Inductive Reasoning in the Logic of Bunched Implications.- Optimal Abstraction on Real-Valued Programs.- Taming the Wrapping of Integer Arithmetic.- Under-Approximations of Computations in Real Numbers Based on Generalized Affine Arithmetic.- A Framework for End-to-End Verification and Evaluation of Register Allocators.- A New Algorithm for Identifying Loops in Decompilation.- Accelerated Data-Flow Analysis.- Abstract Error Projection.- Precise Thread-Modular Verification.- Modular Safety Checking for Fine-Grained Concurrency.- Static Analysis of Dynamic Communication Systems by Partner Abstraction.- Exploiting Pointer and Location Equivalence to Optimize Pointer Analysis.- Hierarchical Pointer Analysis for Distributed Programs.- Semantics-Based Transformation of Arithmetic Expressions.- A Fast Implementation of the Octagon Abstract Domain on Graphics Hardware.- Fixpoint-Guided Abstraction Refinements.- Guided Static Analysis.- Program Analysis Using Symbolic Ranges.- Shape Analysis with Structural Invariant Checkers.- Footprint Analysis: A Shape Analysis That Discovers Preconditions.- Arithmetic Strengthening for Shape Analysis.- Astrée: From Research to Industry.- Magic-Sets Transformation for the Analysis of Java Bytecode.