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 16, 2009

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)

Reading:

Lecture notes [postscript | pdf ]
Some solution notes by Mark Staples may be useful, though they are rather old.
For further reading (optional), here are some suggested books and papers.

Slides [postscript | pdf]
(warning: slides for lectures not yet given might change or be omitted)

Introduction
[ A3 for projection | A4 for printing ]
Formal Specification
[ A3 for projection | A4 for printing ]
Introduction to Primitive Axioms and Rules for Partial Correctness
[ A3 for projection | A4 for printing ]
Further Primitive Rules, Introduction to Derived Rules
[ A3 for projection | A4 for printing ]
More Derived Rules, Mechanizing Program Verification
[ A3 for projection | A4 for printing ]
Proving Programs Terminate
[ A3 for projection | A4 for printing ]
Arrays and FOR-commands, Soundness and Completeness
[ A3 for projection | A4 for printing ]
Program Refinement
[ A3 for projection | A4 for printing ]
Higher-Order Logic
[ A3 for projection | A4 for printing ]
Embedding Programming Logics in Higher Order Logic
[ A3 for projection | A4 for printing ]

Material is examinable if it is presented in lectures!

Examples/Tutorial classes:
Examples classes may be provided, especially if there are not enough supervisors to provide supervisions for everyone.

Strongly recommended seminar: Correctness by Construction of High-Integrity Software
(Rod Chapman, Praxis High Integrity Systems, Wednesday 11 March 2009, 14:15-15:15, Lecture Theatre 1, Computer Laboratory.)

Interesting links

Floyd's orbituary; his seminal 1967 paper Assigning meanings to programs
Hoare's home page at Microsoft; his seminal 1969 paper An axiomatic basis for computer programming
Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems by Edmund M. Clarke Jr.
Zune bug explained in detail
Why - a generic verification condition generator
Scalable Specification and Reasoning: Technical Challenges for Program Logic by Peter O'Hearn
Verified Software: A Grand Challenge
Microsoft SLAM and TERMINATOR projects.
Wikipedia article on Material Implication, the Paradoxes of Material Implication and some classic fallacies
Bibliographic Notes on Hoare Logic compiled by John Reynolds, and the slides for his course at CMU
Collection of Software Bugs and Software Glitches
Peter Homeier's Sunrise system
Design by Contract (a paper by Gary T. Leavens and Yoonsik Cheon)

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.