2IW50 - Algorithms for model checking (2005)
Docent: Jaco van de Pol (mail,www)
Examination:
The examination is open book. Please bring book and course notes!
COURSE MATERIAL
The following book will be used and is mandatory for the course:
Model Checking.
Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled.
MIT Press, ISBN 0-262-03270-8.
Log of Lectures and Slides
Lecture 1:
Read: Chapter 1, Chapter 2.1 and Chapter 3
Final slides Lecture 1
Lecture 2:
Read: Chapter 4.1, 4.1.1.
Read: R.E. Tarjan,
Depth-first search and linear graph algorithms.
SIAM Journal on Computing 1(2):146-160, 1972.
Final slides Lecture 2
Lecture 3:
Read: Chapter 5, Chapter 6.1, Chapter 6.2
Also Chapter 2.2 and Chapter 2.3 are relevant background.
Final slides Lecture 3
Lecture 4:
Read: Chapter 6.3, Chapter 6.4, Chapter 6.6 (up to page 80)
Final slides Lecture 4
Warning: I have rearranged the slides of lecture 3 and 4 a bit, to
avoid the overlaps.
Lecture 5:
Read: Chapter 7 (mu-calculus)
Draft slides Lecture 5
Lecture 6:
Read: Chapter 11 (Equivalences and Preorders)
Draft slides Lecture 6
Lecture 7:
Read: Chapter 13 (Abstraction): 13.1, 13.2, 13.2.1
Draft slides Lecture 7,
Examples Lecture 7
Lecture 8:
This lecture will be devoted to excercises.
Please find a (possibly non-exhaustive list) of topics here:
Topics for examination