Course pages 2013–14
Lecturer: Professor M.J.C. Gordon
No. of lectures: 8
Suggested hours of supervisions: 2
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 and metatheory. Mathematical interpretation of Hoare logic. Deep and shallow semantic embedding. Soundness, completeness and decidability.
- Mechanising program verification. Assertions, annotation and verification conditions. Weakest preconditions and strongest postconditions; their relationship to Hoare logic and its mechanisation.
- Additional topics. Discussion of correct-by-construction methods versus post-hoc verification. Proof of correctness versus property checking. Recent developments in Hoare logic such as separation logic.
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.).