skip to content

Department of Computer Science and Technology

 

Alert:

These pages are currently being updated for 2020/2021

Principal lecturer: 
Prof Larry Paulson
Students: 
MPhil ACS, Part III
Course code: 
L21
Prerequisites: 
Familiarity with basic logic and operational semantics
Hours: 
16

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.

NOTE: If these module is run remotely, students will require a fairly high specification laptop or PC (minimum 8 GB)

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. and 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.

Further Information

Due to COVID-19, the method of teaching for this module will be adjusted to cater for physical distancing and students who are working remotely. We will confirm precisely how the module will be taught closer to the start of term.