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.