Wintersemester 2018/19

Anwendung Formaler Verifikation

Von der Theorie zur Anwendung

Veranstaltungstyp: Seminar
Zielgruppe: Master Informatik
Umfang: 2 SWS / 3 ECTS
Termine: 18.10.2018, 13:00 — 14:00 Uhr in 50.34R211, Auftaktveranstaltung
29.11.2018, 16:00 — 17:00 Uhr, Zwischenvorträge
07.02.2019, 15:45 — 16:30 Uhr in 50.34R301, Hauptvortrag: Rust-Belt
11.02.2019, 16:30 — 18:00 Uhr in 50.34R236, Hauptvorträge: Dependent-Types, Adaptives Randomisiertes Testen
31.03.2019, Abgabe der Ausarbeitung
Veranstaltungsnr.: 2400094
Dozierende:

Alexander Weigl [Organisation]
Prof. B. Beckert
Mihai Herda
Dr. Mattias Ulbrich

Anmeldung: Persönlich oder per E-Mail bei Simone Meinhart (Raum 223, Gebäude 50.34 bzw. simone meinhartXwx3∂kit edu)
Anmeldeschluss: Ende Oktober
Platzvergabe: Reihenfolge nach Eingang der Anmeldung
Alle Plätze vergeben (15.10.2018)
Neue Anmeldungen kommen auf die Warteliste.

Themenbereich

An unserem Lehrstuhl werden formale Methoden für ein breites Spektrum moderner Softwareentwicklung erforscht.

In diesem Seminar werden verschiedene formale Techniken vorgestellt, die dazu beitragen, Programme auf ihre Korrektheit überprüfen zu können. Einige Techniken stellen neue vielversprechende Ansätze vor, andere zeigen auf wie durch geschickten Einsatz und Kombination von Heuristiken existierende Ansätze um Größenordnungen leistungsfähiger gemacht werden können.

Die vorgestellten Ansätze helfen praxisnah, Probleme in Software zu entdecken, zu vermeiden oder zu verhindern.

Aufgabenstellung

Für das Seminar werden von jedem/jeder Teilnehmer/in für eine erfolgreiche Teilnahme folgende Leistungen erwartet:
  • Selbständiges Erarbeiten der Inhalte des vorzustellenden Ansatzes (meist auf Basis eines Papiers im Umfang von etwa 20 Seiten). In regelmäßigen Treffen mit einem/r betreuenden Mitarbeiter/in erhalten Sie hierbei die nötige Unterstützung.
  • Auswahl und Gliederung der Inhalte die in Ihrem Seminarbeitrag präsentiert werden sollen.
  • Kurze Vorstellung Ihrer Gliederung im Plenum.
  • Entscheidung, wie Sie die Inhalte präsentieren wollen.
  • Erstellung der Folien für die Präsentation und gegebenfalls weiterer Materialien.
  • 30-minütiger Hauptvortrag im Plenum (gefolgt von einer etwa 15-minütigen Diskussion).
  • Nach dem Vortrag: Verfassen einer etwa zehnseitigen Ausarbeitung, die die wesentlichen Inhalte des Ansatzes und Ihres Vortrags zusammenfassend darstellt.

Folien

Folien der Auftaktveranstaltung

Vortragsthemen

Die folgende Themenliste soll eine Orientierung über mögliche Themen geben. Wir sind offen für Themenvorschläge aus den Bereichen Formale Verifikation und Methoden. Bei Fragen zu Themen oder Organisation wenden Sie sich bitte an Alexander Weigl <weigl@kit.edu>.

  1. Combining Model Checking and Deduction

    Shankar: Combining Model Checking and Deduction. Handbook of Model Checking.

  2. Verification of Temporal Hyperproperties with HyperMC

    Temporal Logics for Hyperproperties. Michael Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. POST 2014.

  3. How to Prove with Dependent Type Theory? (Theory Behind Coq)

    Adam Chlipala. Certified Programming with Dependent Types.

  4. SAT-based Symbolic Model Checking

    Biere et.al. Symbolic Model Checking without BDDs.

  5. The Modern Way of Model Checking: PDR and IC3

    Aaron Bradley. SAT-Based Model Checking Without Unrolling.

  6. Model Checking with k-Inductiveness and Interpolation

    McMillan. Interpolation and SAT-based Model Checking.

  7. Program Slicing for Verification

    Xu et. al. A brief survey of program slicing.

  8. Learning Invariants with the ICE-Algorithm

    Garg et. al. ICE: A Robust Framework for Learning Invariants.

  9. Reachability Modulo Theories

    Lal and Qadeer. Reachability Modulo Theories.

  10. Horn Clause Solving for Program Verification

    Bjoerner et. al. Horn Clause Solvers for Program Verification.

  11. The Art of Software Testing

    eAnand et. al. An orchestrated survey of methodologies for automated software test case generation.

  12. Predicate Abstraction for Program Verification

    Jhala, Podelski, Rybalchenko. Predicate Abstraction for Program Verification - Safety and Termination. Handbook of Model Checking.

  13. Program Synthesis: Specification-based Creation of Programs

    Bernd Finkbeiner. Synthesis of Reactive Systems (Lecture Notes).