Formale Methoden und Deduktion Prof. Dr. J. Avenhaus

Aufgabenstellung

Im Praktikum geht es um das Erstellen von Korrektheitsbeweisen zu Spezifikationen von Algorithmen, die durch ein positiv/negativ bedingtes Gleichungssystem beschrieben sind. Solche Beweise können häufig nur halbautomatisch erzeugt werden, also durch Unterstützung des Benutzers. Grundlage des Praktikums ist das in der AG entwickelte Beweissystem QUODLIBET. Ziel ist es, zu konkreten Spezifikationen Korrektheitsbeweise zu erstellen und dabei Beweisstrategien zu entwickeln, mit denen man den Automatisierungsgrad des Beweissystems erhöhen kann.

Voraussetzungen

Kenntnisse über induktives Beweisen

Ansprechpartner

Tobias Schmidt-Samoa, 34-407

Vorbesprechung:     Dienstag, 18.02.03, 11:45, 34-420

Impressum

AG Formale Methoden und Deduktion

Fachbereich Informatik

Technische Universität Kaiserslautern