Tutorials.- Model-Based Development: Combining Engineering Approaches and Formal Techniques.- Tutorial on the RAISE Language, Method and Tools.- Model-Based Testing with Spec#.- Formal Engineering for Industrial Software Development – An Introduction to the SOFL Specification Language and Method.- Tutorial: Software Model Checking.- Invited Talks.- Engineering Quality Software.- When Can Formal Methods Make a Real Difference?.- On the Adoption of Formal Methods by Industry: The ACL2 Experience.- A CLP Approach to Modelling Systems.- Full Papers.- Multi-prover Verification of C Programs.- Memory-Model-Sensitive Data Race Analysis.- Formal Models for Web Navigations with Session Control and Browser Cache.- Managing Verification Activities Using SVM.- A General Model for Reachability Testing of Concurrent Programs.- A Knowledge Based Analysis of Cache Coherence.- A Propositional Logic-Based Method for Verification of Feature Models.- Deriving Probabilistic Semantics Via the ‘Weakest Completion’.- CSP Representation of Game Semantics for Second-Order Idealized Algol.- An Equational Calculus for Alloy.- Guiding Spin Simulation.- Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains.- Software Model Checking Using Linear Constraints.- Counterexample Guided Abstraction Refinement Via Program Execution.- Faster Analysis of Formal Specifications.- Bridging Refinement of Interface Automata to Forward Simulation of I/O Automata.- Learning to Verify Safety Properties.- Automatic Extraction of Object-Oriented Observer Abstractions from Unit-Test Executions.- A Specification-Based Approach to Testing Polymorphic Attributes.- From Circus to JCSP.- An Approach to Preserve Protocol Consistency and Executability Across Updates.- A Formal Monitoring-BasedFramework for Software Development and Analysis.- Verifying a File System Implementation.- Verifying the On-line Help System of SIEMENS Magnetic Resonance Tomographs.- Implementing Dynamic Aggregations of Abstract Machines in the B Method.- Formal Proof from UML Models.- Interactive Verification of UML State Machines.- Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity.- From Durational Specifications to TLA Designs of Timed Automata.- Timed Patterns: TCOZ to Timed Automata.