This is a selection, reworked, expanded and with uniform notation, of our principal published papers since 1996 on probabilistic systems and semantics. Its three parts are intended for advanced undergraduates (formal methods), early graduates (semantic techniques) and researchers (new areas) respectively.

• Part I: Probabilistic guarded commands
  • Introduction to pGCL
  • Probabilistic loops: invariants and variants
  • Case studies in probabilistic termination
  • Probabilistic data refinement
• Part II: Semantic structures
  • Theory for the demonic model
  • The geometry of probabilistic programs
  • Proved rules for probabilistic loops
  • The transformer hierarchy
• Part III: Advanced topics
  • The quantitative temporal logic qTL
  • The quantitative algebra of qTL
  • The quantitative mu-calculus qMu

It was published in November 2004. The preface, table of contents and index is given below; on page xi of the preface is a list of the principal published works on which the book is based.