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

• LaTeX Vorlage für Ausarbeitungen

• LaTeX Template for Seminar Papers

• Backstage

• Folien

  • Einführung
  • Präsentieren
  • Grundlagen Logik
  • Wissenschaftliches Schreiben
  • Grundlagen Separation Logic
  • Facebook Infer

• Links zum Thema Präsentieren

  • https://www.microsoft.com/en-us/research/academic-program/give-great-research-talk/
  • http://www.pl-enthusiast.net/2019/01/02/how-to-write-a-conference-talk/
  • https://homes.cs.washington.edu/~mernst/advice/giving-talk.html

• Links zum Thema wissenschaftliches Schreiben

  • https://www.microsoft.com/en-us/research/academic-program/write-great-research-paper/
  • https://www4.informatik.uni-erlangen.de/DE/Lehre/WS06/PS_KVBK/info/Weicker.pdf
  • https://www.uni-muenster.de/imperia/md/content/evtheol/studium_materialien/was_ist_ein_plagiat.pdf

Termine

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

Vorträge des Dozenten:

• 23.4.: Einführung, Themenvergabe
• 30.4.: Wie halte ich eine gute Präsentation?
• 7.5.: (noch offen)
• 14.5.: Wie verfasse ich eine wissenschaftliche Arbeit?

Seminarvorträge der Teilnehmer:

• 21.5.: Kontrakte und Invarianten (Why3)
• 28.5.: Verifikation von objektorientierter Software (Dafny)
• 4.6.: Datenstrukturen: Dynamic Frames (Dafny)
• 11.6.: fällt aus
• 18.6.: Nebenläufigkeit: Separation Logic (Verifast)
• 25.6.: Verifikation von Java mit JML (KeY)

Weiterführende Diskussion:

• 2.7.: fällt aus
• 9.7.: Facebook’s Infer
• 16.7.: fällt aus
• 23.7.: Diskussion Peer-Review

Deadlines

• 16.7.: Upload der vorläufigen Ausarbeitung in Backstage
• bis 23.7.: Kommentare im Backstage
• Dienstag 13.8. 23:59 Uhr: Abgabe der Ausarbeitung

Bewertung

• Vortrag: von 35 Minuten Dauer inklusive praktischer Demo, und anschließender 5-10 minütiger Diskussion
• Ausarbeitung: 20.000 - max. 30.000 Zeichen

Leitung und Kontakt

Prof. Dr. Gidon Ernst

Vorkenntnisse

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

Literatur

• Die jeweilige Literatur zum entsprechenden Tool
• Krzysztof Apt, Frank S. De Boer, Ernst-Rüdiger Olderog. Verification of sequential and concurrent programs. Springer Science & Business Media, 2010.
• Modular specification and verification of object-oriented programs. Springer, 2002.
• Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh, Stephen Magill et al.: Continuous formal verification of amazon s2n. Computer Aided Verification (CAV), 2018. https://github.com/awslabs/s2n
• Zakir Durumeric, Frank Li, James Kasten, Johanna Amann, Jethro Beekman, Mathias Payer, Nicolas Weaver et al.: The matter of heartbleed. In Internet Measurement Conference (IMC), 2014.