Keynote Speech -- Games for Formal Design and Verification of Reactive Systems -- Evolution of Model Checking into the EDA Industry -- Abstraction Refinement -- Invited Speech -- Tools for Automated Verification of Web Services -- Theorem Proving Languages for Verification -- An Automated Rigorous Review Method for Verifying and Validating Formal Specifications -- Papers -- Toward Unbounded Model Checking for Region Automata -- Search Space Partition and Case Basis Exploration for Reducing Model Checking Complexity -- Synthesising Attacks on Cryptographic Protocols -- Büchi Complementation Made Tighter -- SAT-Based Verification of Safe Petri Nets -- Disjunctive Invariants for Numerical Systems -- Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas -- Fair Testing Revisited: A Process-Algebraic Characterisation of Conflicts -- Exploiting Symmetries for Testing Equivalence in the Spi Calculus -- Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors -- Abstraction-Based Model Checking Using Heuristical Refinement -- A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata -- Design and Evaluation of a Symbolic and Abstraction-Based Model Checker -- Component-Wise Instruction-Cache Behavior Prediction -- Validating the Translation of an Industrial Optimizing Compiler -- Composition of Accelerations to Verify Infinite Heterogeneous Systems -- Hybrid System Verification Is Not a Sinecure -- Providing Automated Verification in HOL Using MDGs -- Specification, Abduction, and Proof -- Introducing Structural Dynamic Changes in Petri Nets: Marked-Controlled Reconfigurable Nets -- Typeness for ?-Regular Automata -- Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits -- Mutation Coverage Estimation for Model Checking -- Modular Model Checking of Software Specifications with Simultaneous Environment Generation -- Rabin Tree and Its Application to Group Key Distribution -- Using Overlay Networks to Improve VoIP Reliability -- Integrity-Enhanced Verification Scheme for Software-Intensive Organizations -- RCGES: Retargetable Code Generation for Embedded Systems -- Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets -- First-Order LTL Model Checking Using MDGs -- Localizing Errors in Counterexample with Iteratively Witness Searching -- Verification of WCDMA Protocols and Implementation -- Efficient Representation of Algebraic Expressions -- Development of RTOS for PLC Using Formal Methods -- Reducing Parametric Automata: A Multimedia Protocol Service Case Study -- Synthesis of State Feedback Controllers for Parameterized Discrete Event Systems -- Solving Box-Pushing Games via Model Checking with Optimizations -- CLP Based Static Property Checking -- A Temporal Assertion Extension to Verilog.