Invited Talk.- Model Generation for Horn Logic with Stratified Negation.- Abstraction.- Counterexample Guided Spotlight Abstraction Refinement.- An Experimental Evaluation of Probabilistic Simulation.- An SMT Approach to Bounded Reachability Analysis of Model Programs.- Verification.- Parameterized Tree Systems.- Adapting Petri Nets Reductions to Promela Specifications.- Verification of a Hierarchical Generic Mutual Exclusion Algorithm.- Specification Framework I.- Distributed Semantics and Implementation for Systems with Interaction and Priority.- Checking Correctness of Transactional Behaviors.- Specifying and Verifying Web Transactions.- Application.- Modelling and Analysing the Contract Net Protocol - Extension Using Coloured Petri Nets.- Program Repair Suggestions from Graphical State-Transition Specifications.- Verifying Erlang Telecommunication Systems with the Process Algebra ?CRL.- Specification Framework II.- NQSL - Formal Language and Tool Support for Network Quality-of-Service Requirements.- Timed Mobile Ambients for Network Protocols.- A Specification Framework for Earth-Friendly Logistics.- Theory.- A Hierarchy of Equivalences for Probabilistic Processes.- Multiset Bisimulations as a Common Framework for Ordinary and Probabilistic Bisimulations.- Reliability of Networked Systems.- Detecting Communication Protocol Security Flaws by Formal Fuzz Testing and Machine Learning.- Using SPIN to Detect Vulnerabilities in the AACS Drive-Host Authentication Protocol.- Protocol Modeling with Model Program Composition.