Masterseminar Fehlerfreie Software (deduktive Softwareverifikation)

Anmeldung

In diesem Seminar gibt es 12 Plätze für Masterstudenten. Die Plätze werden zentral mit allen anderen Seminaren nach Studienfortschritt vergeben. Die Anmeldung für Masterstudenten findet ab dem 13.02.2019 bis zum 25.03.2019 zentral per UniWorX statt. Bitte geben Sie dabei Ihre Vorkenntnisse (s.u.) an!

Institutsweite Malus-Regelung: Nach der ersten Vorbesprechung einer jeden Veranstaltung sollen die endgültigen Teilnehmer feststehen. Es gilt, dass jeder Student, der einen Platz im Seminar bzw. Praktikum angenommen hat, diesen Platz auch belegt. Es gibt keine Möglichkeit mehr die Veranstaltung zu verlassen, ohne dass die Teilnahme als nicht erfolgreich (5.0) gewertet wird. Zudem wird eine Malus-Regelung eingeführt, so dass sich das Abspringen bzw. Nicht-Erscheinen in zukünftigen Zentralanmeldungen negativ auswirkt.

Inhalte

Fehlerfreie Software ist ein Wunschtraum aus den Anfängen der Informatik. Programmverifikation mit deduktiven Methoden verspricht diesen Traum zu erfüllen. Diese Techniken werden mittlerweile in großen Firmen wie Microsoft, Google, Amazon und Facebook angewandt, um ausgewählte kritische Software zu spezifizieren und als korrekt nachzuweisen. Ein prominentes Beispiel ist die TLS Bibliothek s2n von Galois/Amazon die als Alternative zu OpenSSL entwickelt wurde um zukünftigen Katastrophen wie Heartbleed vorzubeugen.

Im Seminar werden Grundlagen und fortgeschrittene Techniken vorgestellt und anhand praktischer Beispiele mit einem deduktiven Verifikationstool veranschaulicht.

Organisatorisches

Material

Termine

Das Seminar findet statt jeden Di 14-16 Uhr c.t., Oettingenstr. 67, C 003

Vorträge des Dozenten:

Seminarvorträge der Teilnehmer:

Weiterführende Diskussion:

Deadlines

Bewertung

Leitung und Kontakt

Prof. Dr. Gidon Ernst

Vorkenntnisse

keine (hilfreich: Formale Spezifikation und Verifikation o.ä., Logikprogrammierung)

Literatur