Invited Talks.- Analysis of Systems with Stochastic Process Creation.- Verifying Concurrent Programs with Chalice.- Static Timing Analysis for Hard Real-Time Systems.- Invited Tutorials.- Abstract Interpretation-Based Protection.- Advances in Probabilistic Model Checking.- Building a Calculus of Data Structures.- Regular Papers.- Temporal Reasoning for Procedural Programs.- Improved Model Checking of Hierarchical Systems.- Path-Oriented Reachability Verification of a Class of Nonlinear Hybrid Automata Using Convex Programming.- Complexity Bounds for the Verification of Real-Time Software.- An Abstract Domain to Discover Interval Linear Equalities.- Interpolant Strength.- Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing.- Invariant and Type Inference for Matrices.- Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction.- Automatic Abstraction for Congruences.- Shape Analysis of Low-Level C with Overlapping Structures.- Abstract Threads.- Shape Analysis with Reference Set Relations.- Shape Analysis in the Absence of Pointers and Structure.- An Analysis of Permutations in Arrays.- Regular Linear Temporal Logic with Past.- Model-Checking In-Lined Reference Monitors.- Considerate Reasoning and the Composite Design Pattern.- RGSep Action Inference.- Best Probabilistic Transformers.- Collections, Cardinalities, and Relations.