Modelling Stochastic Systems -- Probabilistic Automata: System Types, Parallel Composition and Comparison -- Tutte le Algebre Insieme: Concepts, Discussions and Relations of Stochastic Process Algebras with General Distributions -- An Overview of Probabilistic Process Algebras and Their Equivalences -- Model Checking of Stochastic Systems -- Verifying Qualitative Properties of Probabilistic Programs -- On Probabilistic Computation Tree Logic -- Model Checking for Probabilistic Timed Systems -- Representing Large State Spaces -- Serial Disk-Based Analysis of Large Stochastic Models -- Kronecker Based Matrix Representations for Large Markov Models -- Symbolic Representations and Analysis of Large Probabilistic Systems -- Probabilistic Methods in State Space Analysis -- Deductive Verification of Stochastic Systems -- Analysing Randomized Distributed Algorithms -- An Abstraction Framework for Mixed Non-deterministic and Probabilistic Systems -- The Verification of Probabilistic Lossy Channel Systems.