Aktuelles

Inhalte

Die Entwicklung zuverlässiger Soft- und Hardware stellt immer noch ein großes Problem dar. Aufgrund der Komplexität moderner Systeme gibt es viele Fehler, die nur in wenigen Systemzuständen oder in bestimmten Interaktionen mit der Umgebung auftreten. Durch Tests sind diese Fehler nur schwer zu finden.  Für kritische Systeme bietet sich daher der Einsatz von Techniken an, die es Entwicklern ermöglichen, Eigenschaften systematisch zu spezifizieren und das fertige System aus der Spezifikation zu generieren oder die Eigenschaften des Systems gegenüber der Spezifikation zu verifizieren.

In dieser Vorlesung werden logische Grundlagen und formale Techniken der Software-Entwicklung behandelt.  Neben dem grundlegenden Verständnis für formale Methoden liegt ein Schwerpunkt auf praktisch anwendbaren Techniken und Werkzeuge zur formalen Spezifikation und Verifikation. Geplant sind die folgenden Themen:

• Einführung in die Computational Logic ACL2 und automatisches Theorembeweisen
• Boole'sche Logik und Erfüllbarkeit, SAT Solving
• Rekursion und induktive Beweise
• Einführung in die Prädikatenlogik und Logiken höherer Ordnung 
• Spezifikation von Systemen
• Ausblick in die Behandlung von zeitbasiertem Verhalten, Model Checking

Termine

Vorlesung (3-stündig)

Übung (2-stündig)

Mündliche Prüfungen

Personen

Dozent

Übungsbleitung

Materialien

Vorlesung

Übungsblätter

Übung

Hörerkreis

Benötigte Vorkenntnisse

Literatur