| Component and Service Oriented Computing |
| A Software Component Model and Its Preliminary Formalisation / Kung-Kiu Lau ; Mario Ornaghi ; Zheng Wang |
| Synchronised Hyperedge Replacement as a Model for Service Oriented Computing / Gian Luigi Ferrari ; Dan Hirsch ; Ivan Lanese ; Ugo Montanari ; Emilio Tuosto |
| System Design |
| Control of Modular and Distributed Discrete-Event Systems / Jan Komenda ; Jan H. van Schuppen |
| Model-Based Security Engineering with UML: Introducing Security Aspects / Jan Jurjens |
| The Pragmatics of Stairs / Ragnhild Kobro Runde ; Oystein Haugen ; Ketil Stolen |
| Tools |
| Smallfoot: Modular Automatic Assertion Checking with Separation Logic / Josh Berdine ; Cristiano Calcagno ; Peter W. O'Hearn |
| Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs / Dennis R. Dams ; Kedar S. Namjoshi |
| Algebraic Methods |
| Beyond Bisimulation: The "up-to" Techniques / Davide Sangiorgi |
| Separation Results Via Leader Election Problems / Maria Grazia Vigliotti ; Iain Phillips ; Catuscia Palamidessi |
| Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation / Wan Fokkink ; Rob van Glabbeek ; Paulien de Wind |
| Model Checking |
| Abstraction and Refinement in Model Checking / Orna Grumberg |
| Program Compatibility Approaches / Edmund Clarke ; Natasha Sharygina ; Nishant Sinha |
| Cluster-Based LTL Model Checking of Large Systems / Jiri Barnat ; Lubos Brim ; Ivana Cerna |
| Safety and Liveness in Concurrent Pointer Programs / Dino Distefano ; Joost-Pieter Katoen ; Arend Rensink |
| Assertional Methods |
| Modular Specification of Encapsulated Object-Oriented Components / Arnd Poetzsch-Heffter ; Jan Schafer |
| Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2 / Patrice Chalin ; Joseph R. Kiniry ; Gary T. Leavens ; Erik Poll |
| Boogie: A Modular Reusable Verifier for Object-Oriented Programs / Mike Barnett ; Bor- Yuh Evan Chang ; Robert DeLine ; Bart Jacobs ; K. Rustan M. Leino |
| Quantitative Analysis |
| On a Probabilistic Chemical Abstract Machine and the Expressiveness of Linda Languages / Alessandra Di Pierro ; Chris Hankin ; Herbert Wiklicky |
| Partial Order Reduction for Markov Decision Processes: A Survey / Marcus Groesser ; Christel Baier |
| Author Index |
| Component and Service Oriented Computing |
| A Software Component Model and Its Preliminary Formalisation / Kung-Kiu Lau ; Mario Ornaghi ; Zheng Wang |
| Synchronised Hyperedge Replacement as a Model for Service Oriented Computing / Gian Luigi Ferrari ; Dan Hirsch ; Ivan Lanese ; Ugo Montanari ; Emilio Tuosto |
