Hoare Logic

Lecturer: Mike Gordon
Taken by: Part II
Number of lectures: 8
Lecture location: Lecture Theatre 2, WGB
Lecture times: 11:00 on Monday, Wednesday and Friday starting on Friday 10 October, 2014

Official web page
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 (only if time): correct-by-construction methods versus post-hoc verification; proof of correctness versus property checking; recent developments such as separation logic. (Official syllabus)
Material is examinable if it is presented in lectures!

Exercises and past exam questions

Examples classes

As there are insufficient supervisors for this course, an examples class will be conducted by Ramana Kumar between 3pm and 4pm on Monday November 10 in LT2. For preparation, Ramana suggests you think about:

Reading

Handout

Slides

The slides presented in the lectures are indicated by a tick to the right of the title. Slides with content that goes beyond what is covered in the 2014/15 course are indicated by a cross . Remember that the examinable material is what is presented in lectures.

Errata

Interesting links