Specification and Verification II

Lecturer: Prof. M.J.C. Gordon (mjcg@cl.cam.ac.uk)

No. of lectures: 12

Prerequisite course: Specification and Verification I

Details below are provisional.

Introduction to formal methods for hardware.

Use of HDLs (e.g. Verilog) versus mathematical logic. Specifying structure and behaviour. Parameterised designs. [4 lectures]

Logical models of transistors.

Simple switch models. Threshold switching models. Unidirectional sequential models. Problems with existing methods. [2 lectures]

Sequential behaviour.

Temporal abstraction. Temporal logic. [2 lectures]

Introduction to proof mechanisation.

Model checking versus interactive proof. State of the art and future prospects. [4 lectures]

Recommended book:

Melham, T.F. (1993). Higher Order Logic and Hardware Verification: Cambridge Tracts in Theoretical Computer Science 31. Cambridge University Press.