Course pages 2020–21 (these pages are still being updated)

# Interactive Formal Verification

**Principal lecturer:** Prof Larry Paulson**Taken by:** MPhil ACS, Part III**Code:** L21**Hours:** 16 (12 lectures and 4 practical classes)**Prerequisites:** Familiarity with basic logic and operational semantics

## Aims

This module introduces students to interactive theorem proving using Isabelle. It includes techniques for specifying formal models of software and hardware systems and for deriving properties of these models.

## Syllabus

- Introduction to higher-order logic and Isabelle/HOL. [2 lectures]
- Recursive datatypes and functions: modelling them in logic, reasoning about them. [2 lectures]
- Reasoning in predicate logic and typed set theory. [2 lectures]
- Inductive Definitions. [1 lecture]
- Introduction to hardware verification: combinational and sequential circuits, registers, etc. [1 lecture]
- Modelling operational semantics definitions and proving properties. [2 lectures]
- Structured proofs. [2 lectures]

## Objectives

On completion of this module, students should:

- possess good skills in the use of Isabelle;
- be able to specify inductive definitions and perform proofs by induction;
- be able to define and use abstract models in verification;
- be able to express a variety of specifications in higher-order logic.

## Coursework

Each candidate will undertake two small formalisations, which will serve as the basis for assessment.

## Practical work

Four supervised practical sessions will allow students to develop skills.

## Assessment

Each student must undertake two small verification projects, each consisting of a practical write-up accompanied by an Isabelle theory file. These will be started during the practical sessions but will probably be completed on the student’s own time. The projects will assess the extent to which each candidate has absorbed the syllabus and developed practical skills. The lecturer will set and mark the assessments. The mark will be reported as a percentage.

Online submission is available from the **Moodle** page *(Only available to Cambridge University staff and students)*

## Recommended reading

Nipkow, T., Paulson, L.C. & Wenzel, M. (2002). *A proof assistant
for higher-order logic*. Springer LNCS 2283.

Krauss, A. *Defining recursive functions in Isabelle/HOL*.

Nipkow, T. (). *Programming and Proving in Isabelle/HOL*.