Automatisierung der Infrastruktur für Termersetzung

Die Erstellung von zuverlässiger Software ist eine herausfordernde Aufgabe. Kleine Fehler in Programmen können dazu führen, dass Berechnungen nicht beendet werden oder widersprüchliche Resultate liefern. Verallgemeinert spricht man hier von (Nicht-)Terminierung und (Nicht-)Konfluenz. Forschungsgruppen in der ganzen Welt entwickeln deshalb Tools zur vollautomatischen Analyse von Terminierung und Konfluenz. Diese Tools treten in jährlichen Wettbewerben gegeneinander um, wobei die Wettbewerbe selber von der Forschungsgemeinschaft organisiert werden. Dieses Österreich-Japan Projekt widmet sich der Entwicklung einer Infrastruktur, um Forscher im Bereich der Terminierungs- und Konfluenz-Analyse zu unterstützen, d.h. sowohl Tool-Autoren als auch Organisatoren von Wettbewerben. Dabei liegt der Fokus auf Termersetzungssystemen, einer einfachen Programmiersprache, die in diesem Bereich häufig verwendet wird. Das Projekt hat drei Hauptziele. Zuerst werden wir eine Software Infrastruktur entwickeln, um Analyse Tools in den genannten Bereichen zu evaluieren. Diese wird die Durchführung von Wettbewerben, wie z.B. der "Confluence Competition" (CoCo) und der "Termination and Complexity Competition" (termCOMP), stark erleichtern. Die Infrastruktur ermöglicht ebenfalls einen unkomplizierten Zugriff auf die teilnehmenden Analyse Tools und auf die Eingaben, die diese bekommen. Weil die Eigenschaften wie Terminierung und Konfluenz unentscheidbar sind, und weil die Analyse Tools selber komplexe Programme sind, können auch hier Fehler passieren, so dass bei den Wettbewerben widersprüchliche Analysen generiert werden. Aufgrund der Komplexität der Analysen kann eine manuelle Inspektion oft nicht sicherstellen, ob eine Analyse fehlerfrei ist. Deswegen werden Prüfprogramme zur Validierung eingesetzt, deren eigene Korrektheit in Beweis-Assistenten formal verifiziert wurde. Da solche formalen Beweise jedoch sehr aufwändig sind, unterstützen die Prüfprogramme nicht alle Arten von Analysen, insbesondere werden Prüfungen für mehrere der neueren Wettbewerbe innerhalb der CoCo kaum unterstützt. Der Ausbau der Prüfungen in diesem Bereich ist deshalb das zweite Ziel dieses Projekts. Das dritte Ziel ist die Entwicklung neuer Analyse Techniken für eine Erweiterung von Termersetzungssysteme, welche darin besteht, dass zusätzlich logische Bedingungen formuliert werden dürfen, was z.B. im Bereich der Programm-Verifikation oft nützlich ist. Neben Konfluenz Analyse für diese erweiterten Systeme sollen auch Techniken aus dem Bereich Induktives Beweisen untersucht werden. Die erwarteten Resultate des Projekts sind eine Software Infrastruktur, die von CoCo und termCOMP genutzt wird und auch für andere Wettbewerbe nützlich sein könnte. Die ausgebauten verifizierten Prüfprogramme werden zu erhöhter Zuverlässigkeit der Analyse Tools führen. Und die erweiterten Termersetzungssysteme führen zu einer besseren Anwendbarkeit in der Programm-Verifikation.