Formal Verification of Reactive Systems
|
Prof. Orna Kupferman
|
| |
| Week |
Thursday Lecture |
Recordings |
| 1 |
22/10/2009
Background and motivation, Floyd's method, Kripke strucure, Temporal logic - LTL, CTL* (154KB) |
Part I, Part II |
| 2 |
29/10/2009
Semantics of CTL*, equivalence of formulae, expressive power, distinguishing power (143KB) |
Part I, Part II |
| 3 |
05/11/2009
Wolper's theorem, LTL is not weaker than CTL (113KB) |
Part I, Part II |
| 4 |
12/11/2009
CTL model checking, Fairness and Fair CTL model checking (125KB) |
Part I, Part II |
| 5 |
19/11/2009
Automata over infinite words - definition, examples, closure properties (150KB) |
Part I, Part II |
| 6 |
26/11/2009
LTL to NBW, introduction to symbolic algorithms (166KB) |
Part I, Part II |
| 7 |
03/12/2009
BDDs, actions on BDDs, Symbolic CTL model checking (143KB) |
Part I, Part II |
| 8 |
10/12/0009
mu-calculus introduction and motivation (134KB) |
Part I, Part II |
| 9 |
no class |
|
| 10 |
24/12/2009
mu-calculus: definition, semantics, bisimulation: definition and example (136KB) |
|
| 11 |
31/12/2009
Checking bisimulation (126KB) |
Part I, Part II |
| 12 |
07/01/2010
Simulation, abstraction, modular verification (153KB) |
Part I, Part II |
| 13 |
14/01/2010
Modular verification for LTL, synthesis (133KB) |
|
| 14 |
21/01/2010
Solving the synthesis problem, overview of what's still out there to learn (167KB) |
|
| |
All Lectures (1.76MB) |
|
|
| |
Useful Links:
|
| |
|