Invited Talks
  Modelling of Complex Software Systems: A Reasoned Overview
  The +CAL Algorithm Language
  Semantic-Based Development of Service-Oriented Systems
Services
  JSCL: A Middleware for Service Coordination
  Analysis of Realizability Conditions for Web Service Choreographies 
  Web Cube
  Presence Interaction Management in SIP SOHO Architecture
Middleware
  Formal Analysis of Dynamic, Distributed File-System Access Controls
  Analysing the MUTE Anonymous File-Sharing System Using the Pi-Caleulus
  Towards Fine-Grained Automated Verification of Publish-Subscribe Architectures
  A LOTOS Framework for Middleware Specification
Composition and Synthesis
  Automatic Synthesis of Assumptions for Compositional Model Checking
  Refined Interfaces for Compositional Verification
  On Distributed Program Specification and Synthesis in Architectures with Cycles
  Generalizing the Submodule Construction Techniques for Extended State Machine Models
Logics
  Decidable Extensions of Hennessy-Milner Logic
  Symbolic Verification - Slicing
  Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness
  A New Approach for Concurrent Program Slicing
  Reducing Software Architecture Models Complexity: A Slicing and Abstraction Approach
Unified Modeling Languages
  Branching Time Semantics for UML 2.0 Sequence Diagrams
  ……
Petri Nets
Parameterized Verification
Real Time
Testing
Author Index