(4 credit points)
Ten one-hour lectures and ten two-hour laboratory sessions
Lecturer: Dr Jim Grundy
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.
Assessment will be by a collection of design and verification based assignments.
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.
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.
This unit will develop the student's understanding of the following ideas:
Upon completion of this unit, the student will be able to:
Students will also gain an appreciation of the value of constructing formal proofs of correctness.
The course will pursue the application of the HOL theorem prover to formal verification in a variety of problem domains, which may include:
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.