A course of 8 lectures prepared
by Mike Gordon for CST
Last given in 2014
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.
Exercises and past exam questions