These lectures are intended to give a broad overview of the most important formal verification techniques. These methods are applicable to hardware, software, protocols etc. and even to checking proofs in pure mathematics, though I will emphasize the applications to verification. Since other lecturers will cover some of the topics in more detail (in particular model checking), my lectures will cover mainly the material on deductive theorem proving, which in any case is my special area of interest. The arrangement of material in these notes is roughly in order of logical complexity, starting with methods for propositional logic and leading up to general theorem proving, then finishing with a description of my own theorem proving program ‘HOL Light’ and 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. Automated theorem proving

5. Arithmetical theories

6. Interactive theorem proving

7. HOL Light

8. Case study of floating-point verification

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.

My book on theorem proving (Harrison 2009) covers many of these topics in more depth, together with simple-minded example code (written in Objective Caml) implementing the various techniques.

http://www.cl.cam.ac.uk/~jrh13/atp/index.html Other useful references for the material here are (Bradley and Manna 2007; Clarke, Grumberg, and Peled 1999; Kroening and Strichman 2008; Kropf 1999; MacKenzie 2001; Peled 2001).