Masterseminar: Fehlerfreie Software (deduktive Softwareverifikation)

• Prüfungen
  • Seminarnote

Aktuelles

• Technische Hinweise zur Videoaufzeichnung

  Windows hat einen eingebauten Screen Recorder (siehe z.B. hier), damit liegen allerdings keine Erfahrungen vor.
  Unter Linux können Sie Videos mit SimpleScreenRecorder aufnehmen, dieses Tool hat sich bewährt.
  Alternativ können Sie selbstverständlich auch Software wie OBS Studio für die Aufnahme nutzen, die allerdings etwas
  mehr Einarbeitungsaufwand erfordert.

  Falls Sie eine Webcam haben, wäre es schön, wenn Sie sich bei Ihrem Vortrag filmen (beachten Sie dann beim Erstellen der Folien, dass keine Inhalte durch Ihr Videobild verdeckt werden). Die einfachste Möglichkeit hierzu ist, ein Videokonferenzsystem zu nutzen, das eine Screen-Sharing- und Aufnahme-Funktion bietet, wie z.B. Zoom (Vertrag mit der LMU vorhanden, nutzbar über https://lmu-munich.zoom.us).

  Falls Sie noch keine Erfahrung mit OBS Studio aber mit Videoschnitt
  haben, bietet es sich an, über Opencast Studio den Bildschirm und die Kamera aufzunehmen und nachher beide Videos zusammenzuführen. Ähnlich möglich wäre es, ein Smartphone zur Videoaufnahme zu nutzen und das Video nachher in das Video der Slides zu integrieren.

  Falls Sie nur den Ton Ihres Vortrag aufnehmen können oder möchten, ist dies z.B. in PowerPoint oder Keynote direkt möglich. Auch Opencast Studio bietet eine einfach zu bedienende Möglichkeit, den Bildschirm zusammmen mit einer Tonspur aufzunehmen. Und natürlich gibt es für jede Plattform viele weitere Programme, die dies unterstützen.

  Bitte verwenden Sie in jedem Fall sofern möglich ein Headset oder ein externes Mikrofon (z.B. Handykopfhöhrer mit eingebautem Mikro, auch haben manche Webcams ein gutes eingebautes Mikro) für die Aufnahme des Tons, da dies eine deutlich bessere Tonqualität ermöglicht.

  Zuletzt verändert: Fr 25 Sep 2020 19:25

• Termine und Fristen

  Abgabe Ausarbeitung: 30. September per Mail

  Abgabe Video: 4. Oktober via https://syncandshare.lrz.de/preparefilelink?folderID=24Rp3TqeGjVFtzH8fWk1i
  - Passwort: “dsv2020”
  - Dauer: ca 25 Minuten

  Zuletzt verändert: Fr 02 Okt 2020 12:35

• Kick-off Meeting (online)

  Wann: Dienstag, 28. April, 14:00 Uhr
  Wo: https://meet.lrz.de/deductive
  Achtung: Bei Beitritt sind Mikro und Cam per default an

  Wie: per Browser (empfohlen: Chromium), oder Jitsi App Android, iOS

  Etiquette für Online Meetings

  • Mikrophon muten und nur zum Sprechen freischalten
  • Bitte mit Kopfhöhrer um Echo zu vermeiden
  • Webcam ist optional, aber willkommen
  • “Hand-Heben” Button und Chat nutzen
  • keine Aufnahmen/Mitschnitte machen

  Zuletzt verändert: Mo 27 Apr 2020 21:52

• Themen und Material veröffentlicht

  Bitte beachten Sie die Informationen und Hinweise zu:

  • Organisatorisches (beinhaltet jezt auch die Lernziele)
  • die Themenübersicht
  • Literaturrecherche, Ausarbeitung (zwei unterschiedliche Foliensätze), Vortrag

  Zur Auffrischung können Sie auch die derzeit online laufende Vorlesung FSV mitverfolgen

  • Videos (bitte nicht weiterleiten/-veröffentlichen)
  • Folienzugriff via FSV1 im Uni2Work

  Zuletzt verändert: Mo 27 Apr 2020 21:52

Beschreibung

Seminarinhalte

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.

Anforderungen

• Selbstständige Einarbeitung in die wissenschaftliche Literatur zum Thema
• Ausarbeitung: 20.000 - max. 30.000 Zeichen (ca 10 Seiten, wahlweise englisch oder deutsch)
• Vortrag: von 35 Minuten Dauer inklusive praktischer Demo wenn möglich, und anschließender 5-10 minütiger Diskussion (gegen Ende des Semesters)

Themen

Interaktives Beweisen

• Higher-Order Logik (Isabelle)
• Konstruktive Typtheorie (Coq)
• Verifikation funktionaler Programme mit Type-Theorie (Agda, Lean)
• Systemmodellierung und Refinement (Event-B)

Programmverifikation

• Kontrakte und Invarianten (Dafny, Why3)
• Intermediate Verifikation Languages (Boogie, Viper)
• Objektorientierte Verifikation (Dafny)
• Information Flow Security (SecC)
• Verifikation von Java (VerCors)
• Verifikation von C (Verifast)
• Verifikation von Python (Nagini)
• Verifikation von Scala (Stainless)
• Verifikation von Rust (Prusti)

Backends

• First-Order Theorem Proving (Vampire)
• Satisfiability Modulo Theory (Z3, CVC4, …)

Institut

Institut für Informatik

Dozent:in

• Gidon Ernst

Kursteilnehmer:innen

10 von 10

Zentralanmeldung

Hauptseminare (Master)

Material

Das Kursmaterial ist nur für Mitglieder des Kurses einsehbar, also z.B. für Teilnehmer:innen, Tutor:innen, Korrektor:innen und Verwalter:innen.

Prüfungen

Name	Anmeldung ab	Anmeldung bis	Termin	Prüfungsanmeldung
Seminarnote				Nicht zur Prüfung angemeldet

Termine

Art	Zeit	Regulärer Raum	Notiz
Seminar	Di 14:00–16:00	Oettingenstr. 67, C003