Course pages 2011–12
Lecturer: Professor M.J.C. Gordon
No. of lectures: 12
Prerequisite courses: Logic and Proof
The aim of the course is to introduce Hoare logic as a basis for the formal specification and verification of imperative programs. A simple language will be used to illustrate core ideas. Both theoretical foundations and the design of mechanized program verifiers will be covered. Some current research activities and challenges will be outlined.
- Formal specification of imperative programs. Formal versus informal methods. Specification using preconditions and postconditions.
- Axioms and rules of inference. Hoare logic for a simple language with assignments, sequences, conditionals and while-loops.
- Loops and invariants. Various examples illustrating loop invariants and how they can be found.
- Partial and total correctness. Hoare logic for proving termination. Variants.
- Additional constructs. Arrays and FOR-commands.
- Semantics. Mathematical interpretation of Hoare logic. Deep and shallow semantic embedding.
- Metatheory. Soundness, completeness and decidability.
- Mechanising program verification. Assertions, annotation and verification conditions. Property checking versus proof of correctness. Interactive versus automatic methods.
- Predicate transformers. Weakest preconditions and strongest postconditions; their relationship to Hoare logic and its mechanisation.
- Program refinement. Transforming specifications to programs using refinement rules. Discussion of correct-by-construction methods versus post-hoc verification.
- Current reseach. Recent developments in Hoare logic such as separation logic.
- Review and conclusions. Review of course material covered. Worked examples. Miscellaneous advice on answering examination questions.
At the end of the course students should
- be able to prove simple programs correct by hand and implement a simple program verifier;
- be familiar with the theory and use of Hoare logic and its mechanisation;
- understand some of the core concepts underlying modern formal program verification.
Huth, M. & Ryan M. (2004). Logic in computer science: modelling and reasoning about systems. Cambridge University Press (2nd ed.).