Lec­ture: Mod­el Check­ing (in Eng­lish)

--- The website is subject to change and constantly updated! ---
[updated ''Examination'' on July 15, 14.00 a.m. ] ---


Lecturer: Prof. Dr. Heike Wehrheim
Tutorial: Jan Haltermannm, Felx Pauck
Laboratory: Arnab Sharma

This lecture will be organized via PANDA. All material regarding this lecture can be found there. Please register in PAUL to attend this course. You will be automatically registered in PANDA after your PAUL registration.

Course in­form­a­tion

The course structure is subject to change.

In general, this course contains five elements:

  • Lectures (probably via screen recordings),
  • tutorial (asynchronously, with possibility for questions),
  • two minitests (probably in Panda) ,
  • laboratory (practical hands-on),
  • each participant of the course works autonomously on a research paper.
  • The course will be taught in English
  • Audience: Students working towards a Master degree in Computer Science
  • Credit points: 4 ECTS (1st part only - old examination regulations) / 6 ECTS (full course - new examination regulations)

Self-as­sess­ment tests for mas­ter lec­tures

The university provides self-assessment tests for master lectures.

Re­com­men­ded Read­ing

[1] E. Clarke, O. Grumberg, D. Peled: Model Checking, MIT Press, 1999.

[2] C. Baier, J.P. Katoen: Principles of Model Checking, MIT Press, 2008.

[3] G.J. Holzmann: The SPIN Model Checker - Primer and Reference Manual, Addison Wesley, 2004.
(see also Spin Webpage)

[4] G.J. Holzmann: The Spin Model Checker, IEEE Trans. on Software Engineering, Vol. 23, No. 5, May 1997, pp. 279-295.

[5] M.B. Dwyer, J. Hatcliff, Robby, C.S. Psreanu, W. Visser: Formal Software Analysis : Emerging Trends in Software Model Checking. Future of Software Engineering Track. Proceedings of the 2007 International Conference on Software Engineering (ICSE 2007), 2007.

[1] will be the basis of a large part of the course, [2] gives a comprehensive introduction to model checking, [3] and [4] describe the SPIN model checker and [5] gives a survey of formal software analyses.

Important Information

--- The website is subject to change and constantly updated ---

[updated on July 15, 14.00 a. m.]


Exam will take place on 30th of July (see Dates)

There is a self-assessment test for this lectures.

Check the dates and the information on Exercises, Tutorials & Labs.