Formale Methoden und Deduktion
Prof. Dr. J. Avenhaus

FB Inf

Parktikum Theorembeweisen Wintersemester 2003/04


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 Valid HTML 4.01!

Letzte Änderung: Wednesday, 26-Oct-05 08:59:18 GMT
www-aven@informatik.uni-kl.de