Note that instead of an oral examination there will be a written exam at the end of the semester.

The first exam will be on the 13.02.2019  from 9:00 - 10:30 in O1. You are required to bring your student identity card to the exam. Additionally you are allowed to bring 1 DIN-A4 paper which has been written to by hand to the exam.
Any other (especially electronic) aids are prohibited.
 

The slides and assignments are uploaded here until PANDA issues are resolved:

Slides1

Slides2

Assignment1

Lecturer: Prof. Dr. Heike Wehrheim
Tutorial: Jürgen König
Laboratory: Manuel Töws

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.

In the course we will study techniques for formally verifying that a system (software or hardware) is correct, i.e. adheres to requirements describing the desired functionality. For describing requirements a particular class of logics, so called temporal logics, will be employed. Temporal logics can be used to describe properties of systems in time. For this class of logics there are algorithms for checking whether a property does or does not hold for a system. If the system under consideration has a finite state space, tools implementing these algorithms can fully automatically carry out the verification.

In the course we will take a look at two temporal logics (LTL and CTL) and their model checking algorithms. We will furthermore work with model checking tools (in particular SPIN) and verify small examples of systems (for instance distributed algorithms) in the exercises.

The course is divided into two parts. The first part takes place during the first two-thirds of the semester. The lecture and the tutorial as well as the exercise sheets are part of this phase. Thereafter, the acquired knowledge is practically used and discussed in the laboratory. Furthermore, each participant of the course works autonomously on a research paper during this phase.

• The course will be taught in English.
• Audience: Students working towards a Master degree in Computer Science.
• The course belongs to the modules:
  • III.1.1 Model-based software development and III.1.5 Analytical Methods in Software Engineering
  • 3.36 Model Checking
    
• Credit points: 4 ECTS (1st part only - old examination regulations) / 6 ECTS (full course - new examination regulations)

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