**Next:**Types

**Up:**Michaelmas Term 2007: 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 reading**

Comprehensive notes supplied.

**Next:**Types

**Up:**Michaelmas Term 2007: Part

**Previous:**Security

**Contents**