Hoare Logic and Model Checking

Aims

The course introduces two verification methods, Hoare Logic and Temporal Logic, and uses them to formally specify and verify imperative programs and systems.

The first aim is to introduce Hoare logic for a simple imperative language and then to show how it can be used to formally specify programs (along with discussion of soundness and completeness), and also how to use it in a mechanised program verifier.

The second aim is to introduce model checking: to show how temporal models can be used to represent systems, how temporal logic can describe the behaviour of systems, and finally to introduce model-checking algorithms to determine whether properties hold, and to find counter-examples.

Current research trends also will be outlined.

Lectures

• Part 1: Hoare logic. 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. Syntax-directedness.
• 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 and metatheory Mathematical interpretation of Hoare logic. Semantics and soundness of Hoare logic.
• Separation logic Separation logic as a resource-aware reinterpretation of Hoare logic to deal with aliasing in programs with pointers.
• Part 2: Model checking. Models. Representation of state spaces. Reachable states.
• Temporal logic. Linear and branching time. Temporal operators. Path quantifiers. CTL, LTL, and CTL*.
• Model checking. Simple algorithms for verifying that temporal properties hold.
• Applications and more recent developments Simple software and hardware examples. CEGAR (counter-example guided abstraction refinement).

Objectives

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 separation logic;
• be able to write simple models and specify them using temporal logic;
• be familiar with the core ideas of model checking, and be able to implement a simple model checker.

Recommended reading

Huth, M. and Ryan M. (2004). Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press (2nd ed.).