Modulcode:	Inf-MS-Sem-FSV
Englische Bezeichnung:	Formal Software Verification
Modulverantwortliche(r):	Prof. Dr. Dirk Nowotka
Turnus:	unregelmäßig (WS13/14 WS14/15 WS15/16)
Präsenzzeiten:	2S
ECTS:	4
Workload:	120 Std.
Dauer:	ein Semester
Modulkategorien:	Sem (MSc Inf)
Lehrsprache:	Englisch
Voraussetzungen:

Kurzfassung:

Selected topics from the area of formal software verification are discussed. The students are expected to choose from a selection of topics. Journal articles, book chapters or other short texts are provided. Building on that material, a written assignment and a talk of 30 mins together with a short discussion provides will be presented.

Lernziele:

• Reading and understanding scientific texts
• Preparation and presentation of a scientific talk over 30 mins
• Written summary of the given topic and presentation of acquired knowledge
• Literature research and a corresponding written text and talk that exceeds the level of a Bachelor seminar

Lehrinhalte:

several formal methods for software verification, for example:

• Model Checking
• SMT- and SAT-Solver
• Reachability problems in large graphs
• Temporal logics
• Timed automata

Weitere Voraussetzungen:

Basics in logics und automata

Prüfungsleistung:

• Frequent and active participation
• Scientific presentation and discussion
• Written summary

Lehr- und Lernmethoden:

The literature research and the preparation of the talk and the written summary should mostly be done independently. The assistants of the Dependable Systems group will provide conceptual and technical help, if needed.

Verwendbarkeit:

Literatur:

The basic literature will be handed out at the beginning of the seminar.

Verweise:

Kommentar: