| Topic | Slides |
| Introduction to models | 1 - 9 |
| Atomic properties | 10 |
| Trees and paths | 11 - 12 |
| Examples of properties | 13 - 16 |
| Reachability | 17 |
| Introduction to model checking | 18 - 26 |
| Symbolic model checking | 27 - 32 |
| Disjunctive partitioning of BDDs | 33 - 35 |
| Generating counter-examples | 36 - 42 |
| Introduction to temporal logic | 43 - 45 |
| Linear Temporal Logic (LTL) | 46 - 58 |
| Computation Tree Logic (CTL) | 59 - 75 |
| CTL model checking | 75 - 83 |
| History of model checking | 84 |
| Expressibility of LTL and CTL | 57 - 58, 85 - 87 |
| CTL* | 88 - 90 |
| Fairness | 91 - 92 |
| Propositional modal μ-calculus | 93 |
| Sequential Extended Regular Expressions (SEREs) | 94 - 95 |
| Assertion Based Verification (ABV) and PSL | 96 - 107 |
| Dynamic verification: event semantics | 108 - 117 |
| Bisimulation | 118 - 120 |
| Abstraction | 121 - 125 |
| Counterexample Guided Abstraction Refinement (CEGAR) | 126 |
| Summary | 127 |