These lectures are intended to give a broad overview of the most important formal verification techniques that are currently used in the hardware industry. They are somewhat biased towards applications of deductive theorem proving (since that is my special area of interest) and away from temporal logic model checking (since there are other lectures on that topic). The arrangement of material is roughly in order of logical complexity, starting with methods for propositional logic and leading up to general theorem proving, then finishing with an extended case study on the verification of a floating-point square root algorithm used by Intel.

1. Propositional logic

2. Symbolic simulation

3. Model checking

4. General theorem proving

5. HOL Light

6. Case study of floating-point verification

My original plan was to lecture on items 1–4 and 6 in the above list. However, since Orna Grumberg presented temporal logic model checking in much more detail, I dropped the lecture on this topic, section 3 here, replacing it by a detailed discussion of HOL Light, which forms section 5 here. The following notes include all this material.

The treatment of the various topics is quite superficial, with the aim being overall perspective rather than in-depth understanding. The last lecture is somewhat more detailed and should give a good feel for the realities of formal verification in this field.

These notes draw on my forthcoming book on automated theorem proving, and simple-minded example code (written in Objective Caml) illustrating many of the techniques described can be found on my Web page:

http://www.cl.cam.ac.uk/users/jrh/atp/index.html