| topic | chapters | slides |
| 1 | Introduction. Propositional Logic. | 2, 3 | slides |
| 2 | Propositional Logic. Satisfiability. | 3 | slides |
| 3 | Satisfiability Checking. | 4 | slides |
| 4 | Polarity. CNF | 4, 5 | slides |
| 5 | CNF and clausal form. Unit propagation | 5 | slides |
| 6 | Optimised Definitional Transformation. DLL. | 5 | slides |
| 7 | SAT and Randomisation. | 8 | slides |
| 8 | Semantic Tableaux. | 9 | slides |
| 9 | BDDs and OBDDs | 10 | slides |
| 10 | OBDD Algorithms. | 10 | slides |
| 11 | Quantified Boolean Formulas. | 11 | slides |
| 12 | Quantified Boolean Formulas. | 11 | slides |
| 13 | Satisfiability Checking for QBF. | 11 | slides |
| 14 | Satisfiability Checking for QBF. | 11 | slides |
| 15 | Propositional Logic of Finite Domains. | 12 | slides |
| 16 | Transition Systems and Temporal Properties. | 13 | slides |
| 17 | Transition Systems and Temporal Properties. Kripke Structures | 13, 14 | slides |
| 18 | LTL | 14 | slides |
| 19 | LTL | 14 | slides |
| 20 | LTL | 14 | slides |
| 21 | LTL | 14 | slides |
| 22 | Model Checking | 15 | slides |
