Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Computer Laboratory
Computer Science Syllabus - Specification and Verification I
Computer Laboratory > Computer Science Syllabus - Specification and Verification I

Specification and Verification I next up previous contents
Next: Types Up: Michaelmas Term 2005: Part Previous: Security   Contents


Specification and Verification I

Lecturer: Professor M.J.C. Gordon

No. of lectures: 12

Prerequisite course: Logic and Proof

This course is a prerequisite for Specification and Verification II.


Aims


The aim of the course is to motivate and illustrate the use of rigorous methods and mechanised tools for reasoning about the functional behaviour of imperative programs. A goal is to show the similarities and differences between hardware and software verification.


Lectures

  • Program specification. Partial and total correctness. Hoare notation. [2 lectures]

  • Program verification. Axioms and rules of Floyd-Hoare logic. Discussion of soundness and completeness. [4 lectures]

  • Mechanised program verification. Annotation. Verification condition generation. [3 lectures]

  • Program refinement. Definition of the refinement relation. Derivation of laws. [1 lecture]

  • Semantic embedding. Deep versus shallow embedding. Shallow embedding of Hoare notation in higher order logic. Programming logic as a special case of general logic. [2 lectures]

Objectives


By the end of the course students should have an understanding of some aspects of the following topics. Partial and total correctness. Hoare notation. Axioms and rules of Floyd-Hoare logic. Soundness and completeness. Mechanised program verification using verification conditions. Program refinement. Semantic embedding in higher order logic. Limitations of program verification.


Recommended books


None (comprehensive notes supplied).



next up previous contents
Next: Types Up: Michaelmas Term 2005: Part Previous: Security   Contents
Christine Northeast
Sun Sep 11 15:46:50 BST 2005