Specification and Verification I

University of Cambridge Computer Laboratory

Principal lecturer: Mike Gordon (mjcg@cl.cam.ac.uk)
Taken by: Part II
Number of lectures: 12
Lecture location: Lecture Theatre 2, WGB
Lecture times: 12:00 on MWF starting Fri 7 Nov 2003


Syllabus
Past exam questions

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

Reading:



Postscript slides (these may change during the course)
 
 
Introduction A3 for projection A4 for printing
Formal Specification A3 for projection A4 for printing
Proof Rules for Partial Correctness A3 for projection A4 for printing
Making Proofs Easier A3 for projection A4 for printing
Mechanizing Program Verification A3 for projection A4 for printing
Proving Programs Terminate A3 for projection A4 for printing
Devising Correct Rules A3 for projection A4 for printing
Program Refinement A3 for projection A4 for printing
Higher Order Predicate Calculus A3 for projection A4 for printing
Deriving Floyd Hoare Logic A3 for projection A4 for printing
VDM, Weakest Preconditions, Dynamic Logic A3 for projection A4 for printing



Additional material in last lecture: Examples and advice on exam technique

Complete set of slides for printing (4 per page, A4 size)

Examples/Tutorial classes: There are not enough supervisors to provide supervisions for everyone, so two afternoon examples class will be run by Joe Hurd. The first class will be 2pm to 4pm on Monday 24 November in FW11 (note: this is on a Monday, even though I previously announced the examples classes would be on Fridays).
Joe will conduct a second class in FW11 at 2pm on Monday 1 December.
Some worked examples and remarks on answering examination questions will also be given in the lectures.

Interesting links

Related course: This course is a prerequisite for Specification and Verification II (web page not yet updated for 2004).

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

Feedback: If high lecturing standards are to be maintained and lower standards to be raised, it is important for lecturers to receive feedback about their lectures. Consequently, we would be grateful if you would complete this questionnaire. A digest of the information will be passed to the Staff-Student Liaison and Teaching Committees.