Lectures on Probabilistic Formal Methods for the 2004 Pernambuco School on Software Engineering
Recife, 23 November to 5 December 2004
Carroll Morgan
University of New South Wales

The presentation explains and motivates a programming logic and semantics that includes both demonic and probabilistic nondeterminism. The former is used to control abstraction and refinement while developing algorithms and systems; the latter allows those systems to contain exhibit probabilistic –that is, quantifiably random– behaviour. Probability is important for random algorithms, for distributed systems and for quantification of risk and cost. The individual lectures will first cover elementary sequential programs (based on Dijkstra's minimally-syntaxed programming language GCL), loops and their associated invariant/variant reasoning tools, and the relational operational model whose existence validates the approach. Later lectures will explore more exotic topics such as probabilistic temporal logic and µ-calculus, and their connection to angelic/demonic/probabilistic games.

The specific topics are listed below, together with pdf slides for viewing (full-sized) and printing (four-to-a-page).

1.   Source-level probabilistic program logic     (for viewing, for printing). 2.   Reasoning about probabilistic loops     (for viewing, for printing). 3.   Example program proofs     (for viewing, for printing). 4.   The underlying relational model     (for viewing, for printing). 5.   Almost-certain termination     (for viewing, for printing). 6.   Probabilistic temporal logic and games     (for viewing, for printing). 7.   Probabilistic µ-calculus and games     (for viewing, for printing). —   (Slides for the SBFM presentation)     (for viewing, for printing).

There is more material here, probably, than there will be time for in the School.

A list of papers for background reading can be found on pages x, xi of the complete draft table of contents linked to from here, and many of the papers referred to in that list can be found here.