|
|
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 |