Termination Tools: Verifikation und Optimierung

Ziel des Projekts ist es, Tools zum automatischen Beweis der Termination von Term-ersetzungssystemen in dreierlei Hinsicht zu verbessern: 1. Zuverlässigkeit: durch formale Verifikation der verwendeten Terminationstechniken mit dem automatischen Beweissystem Isabelle/HOL. 2. Effizienz: durch Anwendung von BDD-Techniken, welche eine kompakte Repräsentation großer Suchräume, wie sie bei leistungsfähigen Terminationstechniken auftreten, erlauben. 3. Anwendbarkeit: durch Modifikation der verwendeten Syntax, so dass auch Aspekte von Logiken höherer Stufe, wie sie beim Funktionalen Programmieren und in automatischen Beweissystemen vorkommen, formuliert werden können. Darüber hinaus ist geplant, 4. durch den Einsatz von Terminationstechniken, wie sie in entsprechenden Tools verwendet werden, in Isabelle/HOL die Klasse der rekursiven Funktionen, deren Termination automatisch bewiesen wird, zu erweitern. Die zentrale Terminationstechnik in Punkt 1 und 4 ist eine Variante der `dependency pair`-Methode basierend auf dem Subtermkriterium von Hirokawa und Middeldorp. In Punkt 2 liegt der Schwerpunkt zunächst auf einer elementaren Version der `dependency pair`-Methode in welcher die `argument filtering`-Technik in Verbindung mit stark monotonen Grundordnungen, wie die lexikographische Pfadordnung, verwendet wird. Schließlich bildet eine neue `uncurrying`-Transformation die Grundlage in Punkt 3. Die unter Punkt 2 und 3 beschriebenen Techniken sollen in das Tyrolean Termination Tool eingebunden werden.

Die Korrektheit von Computersystemen zu beweisen, ist von äußerster Wichtigkeit, vor allem für sicherheitskritische Systeme wie Brandmelder, Fly-by-wire, bemannte Raumfahrt, Kernreaktoren, computergesteuerte Chirurgie, etc. Ein entscheidender Bestandteil, um die Korrektheit zu beweisen, ist zu zeigen, dass ein Computerprogramm ein Ergebnis liefert, da es andernfalls endlos rechnen könnte. Diese Eigenschaft wird als Terminierung bezeichnet und ist im Allgemeinen nicht entscheidbar. Nichtsdestotrotz gibt es Terminierungsbeweiser, welche Terminierung in erstaunlich vielen Fällen automatisch nachweisen können. Im Zuge dieses Projekts konnten Terminierungsbeweiser insofern verbessert werden, dass einerseits neue Terminierungskriterien entworfen wurden und andererseits bestehende Kriterien effizienter implementiert wurden. Es hat sich herausgestellt, dass es vorteilhaft ist, die einzelnen Kriterien nicht mit maßgeschneiderten Algorithmen zu lösen, sondern sie in ein anderes Problem (SMT) umzuwandeln und mit spezialisierten Tools zu lösen. Dieser Ansatz vereinfacht die Implementierung von herkömmlichen Kriterien und reduziert die Laufzeit. Terminierungsbeweiser sind ihrerseits nur Software und können auf Grund von Fehlern falsche Resultate liefern (was auch schon vorgekommen ist). Deshalb gibt es aktuell den Trend zum automatischen zertifizieren von Terminierungsbeweisen, welche von einem Terminierungsbeweiser erstellt wurden. Um dies zu bewerkstelligen, muss jedes Terminierungskriterium welches in einem Beweis verwendet wird, im Theorembeweiser als korrekt bewiesen werden. Dies ist weitaus schwieriger als den Beweis per Hand durchzuführen, weil jeder Beweis in kleine Schritte zerlegt werden muss, welche der Theorembeweiser verstehen kann. Dadurch kann aber ausgeschlossen werden, dass der Beweis fehlerhafte Schritte beinhaltet. In diesem Projekt wurden solche Korrektheitsbeweise für viele Techniken durchgeführt, welche in Terminierungsbeweisern verwendet werden. Dadurch können wir auch zahlreiche Terminierungsbeweise von aktuellen Terminierungsbeweisern zertifizieren.