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:
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com