Course pages 2016–17

**Subsections**

##

Hoare Logic and Model Checking

*Lecturer: Dr D. Mulligan and Dr K. Svendsen*

*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.).