Formal Verification (Lecture notes from Marktoberdorf 2010)

John Harrison.
In Broy, Leuxner and Hoare (eds): "Software and Systems Safety - Specification and Verification", IOS Press 2011, pp. 103-157,

Abstract:

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.

PDF

Bibtex entry:

@INPROCEEDINGS{harrison-mark10,
        author          = "John Harrison",
        title           = "Formal Verification (Lecture notes from
                           Marktoberdorf 2010)",
        editor          = "Manfred Broy and Christian Leuxner and
                           Tony Hoare",
        title           = "Software and Systems Safety - Specification and
                           Verification",
        publisher       = "IOS Press",
        year            = 2011,
        pages           = "103--157"}