Sommersemester 2022

Anwendung Formaler Methoden

Von der Theorie zur Anwendung

Veranstaltungstyp: Seminar
Zielgruppe: Master Informatik
Umfang: 2 SWS / 3 ECTS
Termine: Kurzvorträge: 2.6.2022, 15:45, SR 236
Hauptvorträge: 21.7.2022, 15:45, SR 236
Veranstaltungsnr.: 2400025
Lehrstühle: Anwendungsorientierte Formale Verifikation
Zuverlässige Softwaresysteme in der Automobilindustrie
Dozenten:

Jonas Schiffl [Organisation]
Prof. B. Beckert
Prof. C. Sinz
Philipp Kern
Michael Kirsten
Jonas Klamroth
Dr. Mattias Ulbrich
Alexander Weigl

ILIAS-Kurs: t.b.a.
Anmeldung: persönlich oder per E-Mail bei Jonas Schiffl (Raum 226, Gebäude 50.34 bzw. jonas.schiffl∂kit edu)
Anmeldeschluss: 29.04.2022
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.

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 Jonas Schiffl.

  1. (Linear) Types for 0, 1, or many uses
    Mogensen, T.: Types for 0, 1 or many uses
  2. A Hoare logic for program incorrectness
    Incorrectness logic
  3. Haftung und Verantwortung in einem Blockchain-System
    Accountability in a Permissioned Blockchain: Formal Analysis of Hyperledger Fabric
  4. Modellgetriebene Entwicklung von Smart Contracts
    Towards Model-Driven Engineering of Smart Contracts for Cyber-Physical Systems
  5. Modular Bug-Finding Techniques Moy et al.: Modular Bug-finding for Integer Overflows in the Large
  6. Tight Linear Program Encodings for Neural Network Certification
    General and precise neural network certification via scalable convex hull approximations
  7. Verification of Autoencoders
    Robustness certification with generative models
  8. Improving Branch and Bound Algorithms for Neural Network Verification by utilizing ReLU Dependencies
    Efficient Verification of ReLU-Based Neural Networks via Dependency Analysis
  9. Learning Invariants with ICE and IC3

    Aaron Bradley. SAT-Based Model Checking Without Unrolling.
    Garg et. al. ICE: A Robust Framework for Learning Invariants.

  10. Predicate Abstraction for Program Verification
  11. Reasoning about Strategic Abilities in Multi-Agent Systems
  12. Formalization of Cryptography Using CryptHOL
  13. Graph Neural Networks for SAT Solving

    Bunz and Lamm: Graph Neural Networks and Boolean Satisfiability

  14. Confidentiality by Formal Methods

    Sinha et al.: A design and verification methodology for secure isolated regions. PLDI 2016: 665-681

  15. Verification of Temporal Hyperproperties with HyperMC

    Temporal Logics for Hyperproperties. Michael Clarkson et al, POST 2014.

  16. Specification Mining

    General LTL Specification Mining