Module label | Program Verification |
Modulkürzel | inf407 |
Credit points | 6.0 KP |
Workload | 180 h |
Institute directory | Department of Computing Science |
Verwendbarkeit des Moduls |
|
Zuständige Personen |
|
Prerequisites | Theoretical computer science I and II |
Skills to be acquired in this module | Introduction to methods for proving the correctness of sequential, parallel, and distributed programs. Professional competence The students:
The students:
The students:
The students:
|
Module contents | Program verification is a systematic approach to show the absence of errors in programs. For this purpose desirable behavioural properties of a given program are proven. For instance, a sorting program should only deliver sorted arrays. Partial correctness, termination, and the absence of runtime errors are essential for sequential programs. Additional behavioural properties are of interest for parallel programs: absence of interference, absence of deadlocks, and fair behaviour. The module focuses on the verification of parallel programs. For this purpose classic methods of Hoare's logic are combined with more recent techniques of program transformation. Sequential programs are covered in preparation for this. |
Literaturempfehlungen | essential: "K.R. Apt, E.-R. Olderog, Programmverifikation, Springer-Verlag, 1994'' Or the extended English version: "K.R. Apt, F.S. de Boer, E.-R. Olderog, Verfication of Sequential and Concurrent Programs, Third Edition, Springer-Verlag, 2008'' |
Links | |
Language of instruction | German |
Duration (semesters) | 1 Semester |
Module frequency | irregular |
Module capacity | unlimited |
Modullevel / module level | |
Modulart / typ of module | |
Lehr-/Lernform / Teaching/Learning method | 1VL + 1Ü |
Vorkenntnisse / Previous knowledge | Theoretical computer science I and II |
Form of instruction | Comment | SWS | Frequency | Workload of compulsory attendance |
---|---|---|---|---|
Lecture | 3 | 42 | ||
Exercises | 1 | 14 | ||
Präsenzzeit Modul insgesamt | 56 h |
Examination | Prüfungszeiten | Type of examination |
---|---|---|
Final exam of module | At the end of the lecture period |
Written exam or oral exam |