COMP8033: Mechanical Verification

(4 credit points)
First Semester
Ten one-hour lectures and ten two-hour laboratory sessions

Lecturer: Dr Jim Grundy

Syllabus

This unit introduces students to the concepts and tools necessary for the construction of high-integrity hardware and software systems through computer-aided verification. Beginning with a formalisation of the abstract behaviour of transistors, the course will proceed to examine how to model simple combinatorial and timed circuits, signalling systems, and imperative programs; as well as how to verify their correct operation.

Proposed Assessment

Assessment will be by a collection of design and verification based assignments.

Description

The formalism employed in the course is that of simply-typed higher-order logic, as implemented by the HOL theorem proving system. This is a simple, yet powerful, logic employed on a variety of industrially relevant verification problems.

The unit emphasises the acquisition of practical skills. Students will also learn how to program in the function language ML, and how to use the HOL theorem proving tool. The course includes a major component of laboratory work, for which students will use the department's High-Performance Computing Laboratory of Silicon Graphics workstations.

Rationale

This unit exists to give students an insight into current trends in mechanically applied formal methods. It enables them gain insight into the potential and limits of these techniques as well as developing their own ability to use logic and mathematics as a practical problem solving tool.

Ideas

This unit will develop the student's understanding of the following ideas:

• The role of mathematics in requirements capture.
• The role of mathematics in defining the meaning of languages.
• The definitional approach to mathematics.
• The role of formal proof in verification.

Objectives

Upon completion of this unit, the student will be able to:

• program in the functional language ML;
• specify simple requirements using higher-order logic;
• model the behaviour of simple systems using higher-order logic;
• use the HOL theorem prover to formally verify that a simple system meets its requirements

Students will also gain an appreciation of the value of constructing formal proofs of correctness.

Topics

The course will pursue the application of the HOL theorem prover to formal verification in a variety of problem domains, which may include:

• imperative programming
• functional programming
• digital circuits
• communications protocols

Skills

Students will improve their skills in functional programming and gain new skills in capturing requirements in formal notations. The unit will also develop the students understanding of semantics of programming languages. Specific skills in formal reasoning are a major focus of the unit.

Recommended Reading

• Michael J. C. Gordon and Thomas F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.
• Thomas F. Melham. Higher Order Logic and Hardware Verification, volume 31 of Tracts in Theoretical Computer Science. Cambridge University Press, 1993.
• Lawrence C. Paulson. ML for the Working Programmer. Cambridge University Press, 1991.