Advanced tutorial on model checking
Organised by Javier Esparza and Stephan Merz on 25 June 2002, Adelaide, Australia.
Programme
| Time | Topic |
|---|---|
| 9:00-10:00 | Basics A bit of history A case study: the Needham-Schroeder protocol Linear and branching time temporal logics |
| 10:00-10:30 | Model-checking LTL I The automata-theoretic approach |
| 10:30-11:00 | Coffee break |
| 11:00-11:30 | Model-checking LTL II Partial-order techniques |
| 11:30-12:30 | Model-checking CTL Basic algorithms Binary Decision Diagrams |
| 12:30-14:00 | Lunch |
| 14:00-15:30 | Abstraction |
| 15:30-16:00 | Coffee break |
| 16:00-17:30 | Infinite state spaces Sources of infinity Symbolic search: backward and forward Accelerations and widenings |