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

Worse--and spreading the effect of software flaws far beyond the original customer-- several devastating computer viruses have taken advantage of bugs and defects in common operating systems such as those sold by Microsoft, hobbling thousands of corporate computer networks last year.

[From an article on CNET on August 27, 2002]

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:

The lecture notes contain all examinable material [postscript | pdf ]
Some solution notes by Mark Staples may be useful, though they are quite old.
For further reading (optional), here are some suggested books and papers.

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

Floyd's orbituary
Tony Hoare's home page at Microsoft
Peter Homeier's Sunrise system
High cost of bugs ignites quest for exterminators (an EETimes article)
Overview (Peter Lee) and research project (Andrew Appel) on proof carrying code (PCC)
Peter Lee's Harvard talk entitled Certified Code [Powerpoint format (2.08MB) | PDF format (212KB)]
Touchstone certifying compiler for Java
Design by Contract
Escher Technologies
Buggy software still takes a toll (article on CNET on August 27, 2002)
Why Use B
Some classic fallacies
On the automatic discovery of loop invariants (by A. Ireland, J. Stark)

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.