Sommersemester 2024

Anwendung Formaler Verifikation

Von der Theorie zur Anwendung

Veranstaltungstyp: Seminar
Zielgruppe: Master Informatik
Umfang: 2 SWS / 3 ECTS
Termine: t.b.a.
Veranstaltungsnr.: 2400025
Lehrstuhl: Anwendungsorientierte Formale Verifikation
Dozierende:

Wolfram Pfeifer
Prof. Dr. Bernhard Beckert
Joshua Bachmeier
Philipp Kern
Dr. Michael Kirsten
Jonas Klamroth
Florian Lanzinger
Dr. Romain Pascual
Jonas Schiffl
Samuel Teuber
Dr. Mattias Ulbrich
Dr. Alexander Weigl

Anmeldung: Persönlich oder per E-Mail bei Wolfram Pfeifer (Raum 228, Gebäude 50.34 bzw. wolfram.pfeifer∂kit edu)
Platzvergabe: Reihenfolge nach Eingang der Anmeldung

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.

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 Wolfram Pfeifer.

  1. Justicia: A Stochastic SAT Approach to Formally Verify Fairness
  2. Provable Bounds on the Gradients of Neural Networks
    Shi et al.: Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagation
  3. Provably Bounding Neural Network Preimages
    Kotha et al.: Provably Bounding Neural Network Preimages
  4. Reasoning about Strategic Abilities in Multi-Agent Systems
  5. Formalization of Cryptography Using CryptHOL