Computer Laboratory

Course pages 2011–12

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. Verifying simple functional programs. [1 lecture]
  • Recursive datatypes and functions: modelling them in logic, reasoning about them. [1 lecture]
  • Simplification heuristics. [1 lecture]
  • Logical reasoning: how to generate proofs that involve quantification, case analysis, etc. [2 lectures]
  • Set-theoretic primitives, notation and reasoning methods. [1 lecture]
  • Introduction to hardware verification: combinational and sequential circuits, registers, etc. [2 lectures]
  • Modelling operational semantics definitions and proving properties. [2 lectures]
  • Structured proofs. [2 lectures]

Objectives

On completion of this module, students should:

  • possess basic skills in the use of Isabelle;
  • be able to specify inductive definitions and perform proofs by induction;
  • be able to verify simple hardware circuits;
  • be able to express a variety of specifications in higher-order logic.

Coursework

Each candidate will undertake a small formalisation, 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 a small verification project, delivering a practical write-up accompanied by an Isabelle theory file. It will be started during the practical sessions but will probably be completed on the student’s own time. The project will assess the extent to which each candidate has absorbed the syllabus and develop 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. (). A Tutorial Introduction to Structured Isar Proofs.