Computer Laboratory

Course pages 2015–16

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.

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.

Notes:

L21 Interactive Formal Verification cannot be taken in conjunction with R202 Data Centric Networking or P33 Building an Internet Router in 2012-13.

Class limit: 15 students