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
Additional topics (only if time):
correct-by-construction methods versus post-hoc verification; proof of
correctness versus property checking; recent developments such as
Material is examinable if it is presented in lectures!
Exercises and past exam questions
If there are insufficient supervisors for this course, then it is
hoped that examples classes will be provided instead. Details will be
The slides presented in the lectures are indicated by a
tick ✓ to the right of the title and
slides with content that goes beyond what is covered in the 2014/15
course are indicated by a cross ✗.
The ticks and crosses in the slides (and updated handout) will only
become accurate after the lecture is given. For lectures not yet given
the ticks and crosses are from last year's course. Based on how last
year's course went, I may present a different subset of the material
in this year's course, thus the ticks and crosses may well
change. Remember that the examinable material is what is presented in
lectures, and this won't be finalised until the lectures are actually
These won't be updated after the start of lectures.
will be updated with any changes or corrections made after the start
Second occurrence of "E" in second bullet point on Slide 286 should be "F" (thanks to Rajeev Goré)