Automatische Terminierungs- und Komplexitätsanalyse imperativer Programme

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

Das Ziel ist die Entwicklung von Techniken zur automatischen Terminierungs- und Komplexitätsanalyse von imperativen Programmen in Sprachen wie Java und C. Solche Techniken sindbeim Entwurf und der Verifikation von Programmen von zentraler Bedeutung. In der ersten Phase des Projekts wurde hierzu der folgende Ansatz entwickelt: Zunächst wird (im Front-End des Verfahrens) automatisch ein symbolischer Auswertungsgraph erzeugt, der alle möglichen Läufe des Java- oder C-Programms repräsentiert. Aus diesem Graph wird anschließend ein Programm in einer einfachen Sprache (wie z.B. ein Integer Transitionssystem oder ein Termersetzungssystem) generiert, dessen Terminierung oder Komplexität dann (im Back-End) untersucht wird. Die Ergebnisse der ersten Phase des Projekts zeigen den Erfolg des Ansatzes. In der zweiten Phase soll der Ansatz zu einem praktisch verwendbaren Verfahren weiterentwickelt werden. Dazu sollen im Vorhaben folgende Ziele verfolgt werden: (A) Es existieren wichtige Klassen von Programmen, bei denen die bislang entwickelten Techniken zum Nachweis der Terminierung nicht verwendet werden können. Daher sollen diese Techniken entsprechend erweitert und so modularisiert werden, dass sie auch für große Programme einsetzbar werden. (B) Die Techniken zum Terminierungsnachweis lassen sich so modifizieren, dass damit auch obere Komplexitätsschranken für die Laufzeit von Programmen berechnet werden können. Der in der ersten Projektphase entwickelte Ansatz führt allerdings oft noch zu sehr hohen Schranken, so dass die Präzision und die Einsetzbarkeit des Verfahrens daher deutlich verbessert werden sollen. (C) Darüber hinaus wurden in der ersten Projektphase auch Techniken zur automatischen Berechnung unterer Komplexitätsschranken für die Laufzeit der Back-End Programme entwickelt. Die Aufgabe ist nun,diese Verfahren so weiterzuentwickeln, dass sie auch für Sprachen wie Java und C im Front-End einsetzbar werden. (D) Um ihre Leistungsfähigkeit zu überprüfen, sollen die in (A) – (C) entwickelten Verfahren in unseren Verifikationstools AProVE, KoAT und LoAT implementiert und durch umfangreiche Experimente empirisch evaluiert und mit anderen Systemen verglichen werden.

• DFG-Verfahren: Sachbeihilfen