Formal verification constructs mathematical proofs about the behaviour of computer hardware and software. As a heavy user of mathematical logic, it has strong connections with theoretical computer science.
This mini-course will present a survey of current formal verification methods. Enough detail will be given to establish clear connections with the underlying theory, and to give some idea of the problems facing the field.
Pre-requisities: The mini-course aims to be self contained. Some familiarity with logic will make the going easier.
1. Introduction. Theorem proving. Propositional logic. First-order logic. [slides]
2. Arithmetic. Higher-order logic. [slides]
3. Model Checking. Computation Tree Logic. OBDDs. Symbolic model checking. [slides]
4. Fairness. Linear Time Logic. The propositional mu-calculus. [slides]
5. SAT-solvers. SAT-modulo-theory solvers. [slides]
6. Predicate abstraction. Automatic abstraction refinement. [slides]