Achtung:

Sie haben Javascript deaktiviert!
Sie haben versucht eine Funktion zu nutzen, die nur mit Javascript möglich ist. Um sämtliche Funktionalitäten unserer Internetseite zu nutzen, aktivieren Sie bitte Javascript in Ihrem Browser.

Info-Icon Diese Seite ist nicht in Deutsch verfügbar
Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right) Bildinformationen anzeigen

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right)

Lecture: Model Checking (in English)

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

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-assessment tests for master lectures

The university provides self-assessment tests for master lectures.

Recommended Reading

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

 

Kontakt

Prof. Dr. Heike Wehrheim

Spezifikation und Modellierung von Softwaresystemen

Heike Wehrheim
Telefon:
+49 5251 60-4331
Büro:
O4.225

Jan Haltermann, M.Sc.

Spezifikation und Modellierung von Softwaresystemen

Jan  Haltermann
Telefon:
+49 5251 60-1709
Fax:
+49 5251 60-3993
Büro:
O4.131

Sprechzeiten:

Verfügbarkeit (Arbeitszeiten):
Montag - Freitag
8.30 Uhr bis 15.30 Uhr

Kaleder

Arnab Sharma

Spezifikation und Modellierung von Softwaresystemen

Arnab Sharma
Telefon:
+49 5251 60-5388
Fax:
+49 5251 60-3993
Büro:
O4.131

Felix Pauck

Spezifikation und Modellierung von Softwaresystemen

Felix Pauck
Telefon:
+49 5251 60-1765
Fax:
+49 5251 60-3993
Büro:
O4.128

Sprechzeiten:

Verfügbarkeit (Arbeitszeit):
Montag - Freitag
07:00 bis ~15:30

Die Universität der Informationsgesellschaft