Computer Laboratory

Course pages 2015–16

Hoare Logic and Model Checking

Principal lecturer: Prof Alan Mycroft
Taken by: Part II
Past exam questions

No. of lectures: 12
Suggested hours of supervisions: 3
Prerequisite courses: Logic and Proof

Aims

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

One main 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 thrust is to introduce temporal properties, show how these can describe the behaviour of systems, and finally to introduce model-checking algorithms which determine whether properties hold or find counter-examples.

Current research trends also will be outlined.

Lectures

  • Part 1: 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. Syntax-directedness.

  • Loops and invariants. Various examples illustrating loop invariants and how they can be found. FOR-loops and derived rules. Arrays and aliasing.

  • Partial and total correctness. Hoare logic for proving termination. Variants.

  • Semantics, metatheory, mechanisation Mathematical interpretation of Hoare logic. Soundness, completeness and decidability. 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.

  • Part 2: Specifying state transition systems. Representation of state spaces. Reachable states.

  • Checking reachability properties. Fixed-point calculations. Symbolic methods using binary decision diagrams. Finding counter-examples.

  • Examples. Various uses of reachability calculations.

  • Temporal properties and logic. Linear and branching time. Intervals. Path quantifiers. Brief history. CTL and LTL. PSL for clocked hardware.

  • Model checking. Simple algorithms for verifying that temporal properties hold. Reachability analysis as a special case.

  • 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 Hoare logic and its mechanisation;

  • be able to write properties in a variety of temporal logics;

  • be familiar with the core ideas of model checking.

Recommended reading

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