Invited Talks -- Tests, Proofs and Refinements -- Formal Verification and Biology -- Trust and Automation in Verification Tools -- Model Checking -- CTL Model-Checking with Graded Quantifiers -- Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms -- Computation Tree Regular Logic for Genetic Regulatory Networks -- Compositional Verification for Component-Based Systems and Application -- A Direct Algorithm for Multi-valued Bounded Model Checking -- Software Verification -- Model Checking Recursive Programs with Exact Predicate Abstraction -- Loop Summarization Using Abstract Transformers -- Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions -- Decision Procedures -- Automating Algebraic Specifications of Non-freely Generated Data Types -- Interpolants for Linear Arithmetic in SMT -- SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems -- SMELS: Satisfiability Modulo Equality with Lazy Superposition -- Linear-Time Analysis -- Controllable Test Cases for the Distributed Test Architecture -- Tool Demonstration Papers -- Goanna: Syntactic Software Model Checking -- A Dynamic Assertion-Based Verification Platform for Validation of UML Designs -- CheckSpec: A Tool for Consistency and Coverage Analysis of Assertion Specifications -- DiVinE Multi-Core – A Parallel LTL Model-Checker -- Alaska -- NetQi: A Model Checker for Anticipation Game -- Component-Based Design and Analysis of Embedded Systems with UPPAAL PORT -- Timed and Stochastic Systems -- Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions -- Decidable Compositions of O-Minimal Automata -- On the Applicability of Stochastic Petri Nets for Analysis of Multiserver Retrial Systems with Different Vacation Policies -- Model Based Importance Analysis for Minimal Cut Sets -- Theory -- Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic -- Tree Pattern Rewriting Systems -- Deciding Bisimilarity of Full BPA Processes Locally -- Optimal Strategy Synthesis in Request-Response Games -- Short Papers -- Authentication Revisited: Flaw or Not, the Recursive Authentication Protocol -- Impartial Anticipation in Runtime-Verification -- Run-Time Monitoring of Electronic Contracts -- Practical Efficient Modular Linear-Time Model-Checking -- Passive Testing of Timed Systems.