Course: Verification of Software and Systems

Schedule online course:

Course (Prof. Dr. Stefan Leue)
Monday 10:00 - 11:30 Start: Nov 2
Thursday 10:00 - 11:30

Tutorial (Martin Kölbl)
Friday 11:45 - 13:15 Start: Nov 13

Description:

Teaching Methods

This course takes place as an online course.
Further details on the course will be provided in ILIAS.
Please register in ZEuS for the course, which will register you automatically in ILIAS as well.

Workload

270 hours, of which 84 hours are spent in class and 186 hours of self study

Prerequisites

Successful participation in the courses Modul Informatik I Modul Informatik II Diskrete Strukturen

Even rigorous software design processes cannot ensure fault-free software and systemst. The objective of software verification is to develop and apply automated and complete algorithmic methods that provide proofs that a software artifact meets its specification, or explanatory counterexamples when this is not the case. In this course we will focus on the verification method of model checking. We will introduce Transition Systems as a basic data structure to capture the software and system behavior, branching and linear time temporal logics to formally capture specifications, and suitable model checking algorithms to analyze both software and system models as well as software code.

Learning objectives

Participants will be enabled to use and assess automated software verification technology, in particular model checking. Moreover, they will be enabled to incorporate automated verification in software and system design projects.

Course literature

Ian Sommerville. Software Engineering. 10th edition. Pearson Education Ltd. 2016.
Bernd Brügge, Allen H. Dutoit. Object-Oriented Software Engineering. Using UML, Patterns and Java. 3rd edition, Prentice-Hall, 2009.

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.

Further literature may be announced during the course.

Record of academic assessments

Written final examination, 90 minutes, plus further assignments during the term.
Particulars will be announced during the course.

Remark

This course overlaps with the courses "Model Checking of Software and Systems" and "Advanced Model Checking". Thus, students who have already attended these courses will not receive new credits for the course "Verification of Software and Systems".

In consultation with participants this course will be taught in English (preferred) or German. Course materials are only available in English. Assignments and examinations may be delivered in German or English.

Participants

Bachelor students.

Subject Area

Informatik der Systeme / Angewandte Informatik

Offering Suitable for Participants from Other Programs and Subject Areas

All

Credits

ECTS-points: 9

Weekly teaching hours

SWS: 4

Course: Verification of Software and Systems