inf408 - Algorithms for Software Verification (Complete module description)
Module label | Algorithms for Software Verification |
Modulkürzel | inf408 |
Credit points | 6.0 KP |
Workload | 180 h |
Institute directory | Department of Computing Science |
Verwendbarkeit des Moduls |
|
Zuständige Personen |
|
Prerequisites | |
Skills to be acquired in this module | Algorithms are presented that enables an automatic analysis and verification of complex structures as used in software systems. In the exercises these algorithms will be implemented and applied to case studies. Professional competence The students:
to examples
Methodological competence The students:
Social competence The students:
Self-competence The students:
|
Module contents | Software systems consist of complex data and control structures and growing state spaces, which makes testing their correctness difficult. The big challenge for computer science is the development of automatic methods to analyse and to verify software systems’ properties. In this course, algorithms for program analysis and model checking are presented and applied. The algorithms process transition systems generated from software and use abstraction techniques for data and transitions to make the state spaces analysable. Topics: Kripke structures, transition systems, temporal logic CTL and CTL*, fixed-point algorithms for recursive CTL-operators, model checking algorithms for CTL, simulation and bisimulation of Kripke structures, theorems on the preservation of properties under (bi-) simulations, existential und universal abstraction of Kripke structures, counterexample-guided abstraction refinement (CEGAR method) |
Literaturempfehlungen |
|
Links | |
Language of instruction | German |
Duration (semesters) | 1 Semester |
Module frequency | unregelmäßig |
Module capacity | unlimited |
Form of instruction | Comment | SWS | Frequency | Workload of compulsory attendance |
---|---|---|---|---|
Lecture | 2 | SoSe oder WiSe | 28 | |
Exercises | 2 | SoSe oder WiSe | 28 | |
Präsenzzeit Modul insgesamt | 56 h |
Examination | Prüfungszeiten | Type of examination |
---|---|---|
Final exam of module | First week of lecture-free period |
Written exam or oral exam |