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.