Formale Spezifikation und Verifikation von Software

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.