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.



Exercises and past exam questions