Course pages 2016–17
Interactive Formal Verification
Principal lecturer: Prof Larry Paulson
Taken by: MPhil ACS, Part III
Hours: 16 (12 lectures and 4 practical classes)
Prerequisites: NB: Not offered in 2017-2018. Familiarity with basic logic and operational semantics
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.
- 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]
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.
Each candidate will undertake two small formalisations, which will serve as the basis for assessment.
Four supervised practical sessions will allow students to develop skills.
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.
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.
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