Hoare Logic

A course of 8 lectures prepared by Mike Gordon for CST Part II
Last given in 2014 (webpage); now discontinued.

Summary: Program specification: partial and total correctness. Hoare notation. Axioms and rules of Hoare logic. Soundness and completeness. Mechanised program verification: verification conditions, weakest preconditions and strongest postconditions. Additional topics: correct-by-construction methods versus post-hoc verification; proof of correctness versus property checking; recent developments such as separation logic.

Reading

Handout (introductory material + slides).
1up handout.
Notes.

Slides

Topics and corresponding slides (PDF).
All slides with one slide per page.
All slides with four slides per page (same as body of handout, but size of slides slightly adjusted).

Exercises and past exam questions

The first 16 exercises in this exercise list have some solution notes.
There are also some past exam questions that are relevant to this course (eventually needs to be updated with 2015 questions).

Sources

HL.tar.gz (README)