Specification and Verification I

Lecturer: Mike Gordon
Taken by: Part II
Number of lectures: 12
Lecture location: Lecture Theatre 2, WGB
Lecture times: 12:00 on Mon, Wed & Thu starting Fri Jan 15, 2010

Summary: Program specification: partial and total correctness. Hoare notation. Axioms and rules of Hoare logic. Discussion of soundness and completeness. Mechanised program verification: verification conditions. Program refinement. Semantic embedding in higher order logic.
(Official syllabus)

Past exam questions
(warning: old questions may contain material not examinable in the current course)


[A3 postscript (for projection) | A4 pdf | A4 pdf (4 slides per page)]
(warning: slides for lectures not yet given might change or be omitted)

Material is examinable if it is presented in lectures!

Interesting links

Related course: This course is a prerequisite for Specification and Verification II

Acknowledgement: Some of the teaching materials in this course were prepared by Dr Paul Curzon.