*Lecturer: Professor M.J.C. Gordon*
(`mjcg@cl.cam.ac.uk`)

*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. Weakest preconditions. Semantic embedding in higher order logic. Limitations of program verification. Problems of reasoning about C programs.

**Recommended books**

None (comprehensive notes supplied).