Viele sicherheitskritische Systeme sind inzwischen Software-gesteuert und Software-Korrektheit daher essentiell. Andererseits ist es praktisch unmöglich, Eigenschaften eines Systems zu garantieren und die Abwesenheit von Fehlern durch Standard-Softwareengineering-Praktiken wie Code-Review, systematisches Testen und gutes Software-Design allein zu erreichen.

Im Bereich der Formalen Methoden sind jedoch inzwischen verschiedene mathematische Techniken und Werkzeuge verfügbar, die eine automatische Analyse von Systemen und Software ermöglichen.

Die Anwendung dieser vollautomatischen Techniken wird typischerweise algorithmische Verifikation genannt.

In diesem Seminar sollen aktuelle Arbeiten zur algorithmischen Verifikation behandelt werden, insbesondere neue Algorithmen und deren Implementation in vollautomatischen Software-Analyse-Werkzeugen. Es sollen auch Beispiele diskutiert werden, in denen diese Techniken erfolgreich angewandt wurden.

Fachlich soll dieses Seminar Studierende in die Lage versetzen, vollautomatische Verifikationstechniken und die dahinterstehenden Algorithmen in der eigenen Entwicklungstätigkeit einzusetzen und einen Nachweis der Korrektheit von Programmen zu führen.

Neben den inhaltlichen Aspekten sowie Techniken des wissenschaftlichen Arbeitens werden in dieser Veranstaltung auch Schlüsselqualifikationen wie Literaturrecherche und Präsentationstechniken vermittelt.

90h = 3 ECTS