Invited Paper.- Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming.- Numerical Abstraction.- Scalable Analysis of Linear Systems Using Mathematical Programming.- The Arithmetic-Geometric Progression Abstract Domain.- An Overview of Semantics for the Validation of Numerical Programs.- Invited Talk.- The Verifying Compiler, a Grand Challenge for Computing Research.- Verification I.- Checking Herbrand Equalities and Beyond.- Static Analysis by Abstract Interpretation of the Quasi-synchronous Composition of Synchronous Programs.- Termination of Polynomial Programs.- Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement.- Invited Talk.- Abstraction for Liveness.- Heap and Shape Analysis.- Abstract Interpretation with Alien Expressions and Heap Structures.- Shape Analysis by Predicate Abstraction.- Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists.- Purity and Side Effect Analysis for Java Programs.- Abstract Model Checking.- Automata as Abstractions.- Don't Know in the ?-Calculus.- Model Checking of Systems Employing Commutative Functions.- Model Checking.- Weak Automata for the Linear Time ?-Calculus.- Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties.- Minimizing Counterexample with Unit Core Extraction and Incremental SAT.- I/O Efficient Directed Model Checking.- Applied Abstract Interpretation.- Verification of an Error Correcting Code by Abstract Interpretation.- Information Flow Analysis for Java Bytecode.- Cryptographic Protocol Analysis on Real C Code.- Bounded Model Checking.- Simple Is Better: Efficient Bounded Model Checking for Past LTL.- Optimizing Bounded Model Checking for Linear Hybrid Systems.- Verification II.- Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives.- Generalized Typestate Checking for Data Structure Consistency.- On the Complexity of Error Explanation.- Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs.