University of Konstanz
Chair for Software Engineering
Prof. Dr. Stefan Leue

Course: Model Checking of Software


Course Material

Course Organization  

The course consists of lectures, tutorials, and a mini-project in which you have a chance to work with the SPIN model checker. You will get a 0.3 bonus for your final exam grade if you can achieve no less than 80% of the total points for the assigned exercises.

Lecture Slides

Slides are usually published after they are covered by the lectures.


The solutions to each assignment will be presented at the tutorial on the same day (Mo 16:15-17:45, D 247) as the deadline for that assignment.

Publishing Date Assignment # PDF Deadline for Submission
29.04.2010 1 pdf 5.05.2010, 24:00
06.05.2010 2 pdf 19.05.2010, 24:00
20.05.2010 3 pdf 26.05.2010, 24:00
27.05.2010 4 pdf 2.06.2010, 24:00
10.06.2010 5 pdf 16.06.2010, 24:00
17.06.2010 6 pdf 23.06.2010, 24:00
24.06.2010 7 pdf 30.06.2010, 24:00
01.07.2010 8 pdf 07.07.2010, 24:00
07.07.2010 9 pdf --

Mini Course Project

A short description of the project is available here: project description.

Further material: Overview of the SIP Protocol.

The tutorial on April 29 will give an introduction to the project and discuss organizational issues.



Master-level course. Open to Bachelor-level students.

Subject Area

Informatik der Systeme / Angewandte Informatik

Contents / Syllabus

The course will introduce into explicit state model checking for reactive software systems. Model checking is an algorithmic, automated technique for the behavioral analysis of soft- and hardware systems. We will illustrate the algorithmic foundations of this technique, present the SPIN tool, and address advanced topics. The accompanying project will address the modeling and analysis of an industrial case-study. Participants are expected to possess a basic knowledge in programming, concurrent systems, automata theory and logic.


Further literature will be announced during the course.


SWS: 3+2
ECTS-points: 8