--- 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.

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)

The university provides self-assessment tests for master lectures.

[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.