2IW50 - Algorithms for model checking (2006)
Docent: Jaco van de Pol (mail,www)
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.
PLANNING
Courses:
Trimester 1, block A: 8 sept - 6 okt, fridays, 10:45 - 12:30, HG 6.96
Trimester 1, block B: 20 oct - 17 nov, fridays, 10:45 - 12:30, HG 6.96
Examination:
The examinations will be open book. Please bring book and course notes!
Trimester 1, block B: 24 nov, 14:00 - 17:00
Trimester 2, block C: 1 feb, 9:00 - 12:00
Old examinations:
November 2005,
January 2006,
LATEST NEWS
* A few typos on the final slides of lectures 6 and 9 have been corrected.
* On the last lecture (November 17) I will be
available to answer questions on the course material.
(Same time/place: HG 6.96, 10:45-12:30)
* Don't forget to register for the examination, and
don't forget to bring the book and the slides to this
open book exam.
Log of Lectures and Slides
Lecture 1:
Read: Chapter 1, Chapter 2.1 and Chapter 3
Final Slides Lecture 1
(B&W)
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
(B&W)
Lecture 3:
Read: Chapter 2, Chapter 6.1, Chapter 6.2
Also Chapter 5 is relevant background (covered in 2R880).
Final Slides Lecture 3
(B&W)
Lecture 4:
Read: Chapter 6.3, Chapter 6.4, Chapter 6.6 (up to page 80)
Final slides Lecture 4
(B&W)
Lecture 5:
Read: Chapter 7 (mu-calculus)
Final slides Lecture 5
(B&W)
Lecture 6:
Boolean Equation Systems (not in the book).
Further reading (optional): Angelika Mader,
Verification of
Modal Properties Using Boolean Equation Systems, PhD thesis.
Final slides Lecture
6
(B&W)
Lecture 7:
Read: Chapter 11 (Equivalences and Preorders)
Final slides Lecture
7
(B&W)
Lecture 8:
Read: Chapter 13 (Abstraction): 13.1, 13.2, 13.2.1
Final slides Lecture 8
(B&W)
Lecture 9:
Confluence (extra material, no handouts)
Further reading (optional): S.C.C. Blom and J.C. van de Pol, State Space Reduction by Proving Confluence, CAV 2002, LNCS 2404.
Final slides Lecture 9
(B&W)
(See also
here
for the slides of the lectures in 2005)