| 1 | -- | 3 | Antonio Cerone, Herbert Wiklicky. Preface |
| 5 | -- | 31 | Marta Z. Kwiatkowska, Gethin J. Norman, David Parker. Quantitative Analysis With the Probabilistic Model Checker PRISM |
| 33 | -- | 55 | Gilles Barthe, Tamara Rezk, Martijn Warnier. Preventing Timing Leaks Through Transactional Branching Instructions |
| 57 | -- | 77 | Walter Binder, Jarle Hulaas. Using Bytecode Instruction Counting as Portable CPU Consumption Metric |
| 79 | -- | 96 | Yuxin Deng, Tom Chothia, Catuscia Palamidessi, Jun Pang. Metrics for Action-labelled Quantitative Transition Systems |
| 97 | -- | 116 | Christel Baier, Pedro R. D Argenio, Marcus Größer. Partial Order Reduction for Probabilistic Branching Time |
| 117 | -- | 133 | Volker Gruhn, Ralf Laue. Patterns for Timed Property Specifications |
| 135 | -- | 159 | Dan Hirsch, Alberto Lluch-Lafuente, Emilio Tuosto. A Logic for Application Level QoS |
| 161 | -- | 175 | Rocco De Nicola, Joost-Pieter Katoen, Diego Latella, Mieke Massink. Towards a Logic for Performance and Mobility |
| 177 | -- | 193 | Ruggero Lanotte, Andrea Maggiolo-Schettini, Angelo Troina. A Classification of Time and/or Probability Dependent Security Properties |
| 195 | -- | 212 | Annabelle McIver, Carroll Morgan. A Novel Stochastic Game Via the Quantitative ::::mu::::-calculus |
| 213 | -- | 239 | Gul A. Agha, José Meseguer, Koushik Sen. PMaude: Rewrite-based Specification Language for Probabilistic Object Systems |
| 241 | -- | 257 | Igor Siveroni. Filling Out the Gaps: A Padding Algorithm for Transforming Out Timing Leaks |
| 259 | -- | 277 | Verena Wolf, Christel Baier, Mila E. Majster-Cederbaum. Trace Machines for Observing Continuous-Time Markov Chains |