Course: Model Checking of Software and Systems

Schedule

  • Course (Prof. Dr. Stefan Leue)
    Monday  15:15 - 16:45  Room: PZ 901      Start: Oct 22
    Thursday  10:00 - 11:30   Room: PZ 901    
  • Tutorial  (Martin Kölbl)
    Wednesday  11:45 - 13:15  Room:  PZ 901     Start: Oct 31

Description

Workload

300 hours, which includes 90 hours of presence in the lectures and tutorials and 210 hours of self-study.

Prerequisites

Bachelor level background in programming, algorithms, concurrent systems, automata theory, graph theory and logic.

Contents

The course will introduce into model checking for reactive software and 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 aim at the modeling and analysis of an industrial case-study.

Learning objectives

It is the goal of the course to enable students to understand and assess the efficiency and practical applicability of model checking technology. It is a further goal to exemplify to students that model checking is implemented in tools, and that these can be applied to practical, industrial-strength case studies. This will enable them to decide about an adequate use of model checking technology when conducting their own software and systems development projects, or to pursue further research in this area.

Course literature

E. Clarke, O. Grumberg and D. Peled, Model Checking, MIT Press, 1999

C. Baier and J.-P. Katoen, Principles of Model Checking, MIT Press, 2008

G. Holzmann, The SPIN Model Checker - Primer and Reference Manual, Addison Wesley, 2003

Further literature will be announced during the course.

Record of academic assessments

Final written examination (90 mins) or oral examination (30 mins.) Participants achieving at least 80% of the marks that can be obtained in the assignments will earn a 0.3 point grade bonus.

Remark

se.uni-konstanz.de

This course is taught in English.

Participants

Bachelor / Master students. 
 

Subject Area

Informatik der Systeme / Angewandte Informatik 
 

Offering Suitable for Participants from Other Programs and Subject Areas

All 
 

Credits

ECTS-points: 10

Weekly teaching hours

SWS: 4