Skriptorium
Diplomarbeit
Automatische Synthese von Relationen für Terminierungsbeweise
Diplomarbeit bei Prof. Dr. J. Giesl
[ PDF ] [ BibTeX-Eintrag ]
[ Vortragsfolien Zwischenvortrag ] [ Vortragsfolien Abschlußvortrag ]
Mit dem am Lehr- und Forschungsgebiet I2 entwickelte Verifikationssystem AProVE lassen sich Terminierungsbeweise für funktionale Programme und Termersetzungssysteme durchführen. Ziel der Arbeit ist es, weitere Verfahren zur Synthese geeigneter Basisordnungen zu entwickeln, zu implementieren und zu integrieren. Dabei ist u.a. das Size-Change-Prinzip zum Terminierungsnachweis im Basisverfahren, sowie im kombinierten Verfahren mit Dependency Pairs, zu verbessern. Desweiteren soll die Knuth-Bendix Ordnung als Basisordnung implementiert und integriert werden. Weitere Ziele sind die Evaluierung der implementierten Verfahren insbesondere im Vergleich mit anderen Basisordnung und in Kombination mit anderen Terminierungstechniken. Abschließend wird ein Verfahren vorgestellt, um die Informationen eines Terminierungsbeweises zu kapseln und für den Benutzer ansprechend und verständlich aufgearbeitet wiederzugeben (zum Beispiel als natürlichsprachliches LaTeX-Dokument).
Seminararbeiten
Java-Verifikation mit »Isabelle«
Seminar »Verifikation von Programmen«
Prof. Dr. J. Giesl – Wintersemester 2001/2002
[ PDF ] [ Vortragsfolien ] [ BibTeX-Eintrag ]
Das Verifikationswerkzeug Isabelle führt Beweise auf Basis einer higher-order-logic (HOL) durch. Will man beispielsweise Beweis an der Programmiersprache Java durchführen, so ist eine Modellierung der Programmiersprache Java in dieser HOL notwendig. Die Arbeit erläutert eine Möglichkeit der Modellierung und zeigt am Beispiel eines Beweises der Typkorrektheit von Java eine Einsatzmöglichkeit des Modells auf.
G-Maschine: Graphersetzung als Basis der Funktionalen Programmierung
Seminar »XML-Schema und andere Typen bei Graphen«
Prof. Dr. M. Nagl – Sommersemester 2002
[ PDF ] [ Vortragsfolien ] [ BibTeX-Eintrag ]
Im Gegensatz zu imperativen Programmiersprachen basieren funktionale Sprachen nicht auf Schleifen und Zuweisungen. Die Ausführungssemantik besteht vielmehr aus Ersetzungs- und Reduktionsregeln. Dadurch können bei der Auswertung sehr schnell Graphstrukturen entstehen. Die G-Maschine ist eine abstrakte Maschine, die funktionale Ausdrücke mittels Graphreduktion auswertet.