Course material 2010–11
Lecturer: Professor M.J.C. Gordon
No. of lectures: 8
Prerequisite courses: Logic and Proof
The aim of the course is to show how Hoare logic provides a basis for the formal specification and verification of imperative programs. A simple language will be used to illustrate core ideas. 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.
- Semantics. Mathematical interpretation of Hoare logic. Soundness and relative completeness.
- Mechanising program verification. Weakest preconditions and strongest postconditions. Verification conditions.
- Automated theorem proving. Property checking versus proof of correctness. Interactive versus automatic methods.
- Current reseach. 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 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.).