20-00-0794-iv Formale Spezifikation und Verifikation von Software

Lehrende: Prof. Dr. rer. nat. Reiner Hähnle

Veranstaltungsart: Integrierte Veranstaltung

Orga-Einheit: FB20 Informatik

Anzeige im Stundenplan: FSAV

Fach:

Anrechenbar für:

Semesterwochenstunden: 4

Unterrichtssprache: Englisch

Min. | Max. Teilnehmerzahl: - | -

Digitale Lehre:
Die Kurssprache ist Englisch.
Die Kurswebseite ist unter https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1018 verfügbar.

Lehrinhalte:
In dieser Vorlesung behandeln wir fortgeschrittene Themen aus dem Gebiet der formalen Spezifikation und deduktiven Verifikation objekt-orientierter Software.

Der Kurs deckt insbesondere folgende Themen ab:
* Spezifikation von Interfaces und Klassen mit Hilfe von Queries, Ghost- und Modellfeldern;
* Das "Framing" Problem: Statische und dynamische Frames
* Programmlogik und -kalkül als Grundlage der deduktiven Verifikation
* Spezifikation und Verifikation rekursiver Methoden und Schleifen
* Modulare Verifikation: Sichtbarkeiten, Beweis und Anwendung von Framing-Eigenschaften
* Automatische Erzeugung von Schleifeninvarianten und Methodenverträgen

Der Kurs behandelt vorwiegend sequentielle Programme. Es werden aber auch aktuelle Ansätze zur Spezifikation und Verifikation nebenläufiger bzw. verteilter Software diskutiert.

Für fast alle Themen wird deren praktische Anwendung mit Hilfe geeigneter Tools demonstriert und in den Übungen vertieft.

Voraussetzungen:
Grundlagenwissen über Logik erster Ordnung
Inhalt der Vorlesungen:

• Formale Methoden im Softwareentwurf
  
• Aussagenlogik und Prädikatenlogik
  

Zusätzliche Informationen:
Kurswebseite: https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1018

Online-Angebote:
Kurswebseite: https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1018