Automatische Terminierungsanalyse für funktionale, imperative und logische Programmiersprachen

• Antragsteller: Professor Dr. Jürgen Giesl
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2005 bis 2013
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5457086

Der Terminierungsnachweis ist eine der Hauptaufgaben der Programmverifikation. In letzter Zeit wurden große Fortschritte bei der automatischen Terminierungsanalyse von Termersetzungssystemen erzielt. Hingegen gibt es bei realen Programmiersprachen kaum Ansätze zum automatischen Terminierungsbeweis. Unser Ziel ist daher, neue Entwicklungen aus dem Gebiet der Termersetzung für existierende Programmiersprachen und somit für praktische Anwendungen nutzbar zu machen. Dadurch wird die Leistungsfähigkeit und Anwendbarkeit der automatischen Terminierungsanalyse substantiell erhöht. Das offene Problem der Übertragung von Ansätzen aus der Termersetzung auf Programmiersprachen wird in den drei Beiträgen des Projekts gelöst: (A) Es sollen neue Transformationen von Programmen in Termersetzungssysteme entwickelt werden, die für den Einsatz in der Terminierungsanalyse optimiert sind. Dies erlaubt die direkte Anwendung von Verfahren aus der Termersetzung zum Terminierungsnachweis von Programmen. (B) Die Terminierungsanalysetechniken für Termersetzungssysteme müssen deutlich erweitert werden, um auf den Systemen erfolgreich zu sein, die aus realen Programmiersprachen entstehen. (C) Mit den Ergebnissen aus (A) und (B) sollen existierende Tools zur Terminierungsanalyse von Termersetzungssystemen auf Programmiersprachen erweitert und praktisch evaluiert werden.

• DFG-Verfahren: Sachbeihilfen