Next: Digital Communication II
Up: Michaelmas Term 1999: Part
Previous: Artificial Intelligence
Lecturer: Prof. 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
At 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).
Next: Digital Communication II
Up: Michaelmas Term 1999: Part
Previous: Artificial Intelligence
Christine Northeast
Mon Sep 20 10:28:43 BST 1999