Automatische Komplexitätsanalyse mittels Transformationen

Dieses Projekt behandelt die Komplexitätsanalyse von Programmen. Dies ist ein überaus wichtiges Thema, da die Komplexiät einen Programmes gewissermaßen seine Nützlichkeit bestimmt. Wir sind hier an einer automatischen Analyse interessiert, die wie eine "Knopfdruck"-Technik funktioniert: Wir drücken einen Knopf und das Tool gibt uns detailiert Auskunft über die Komplexität des Eingabeprogramms. Darüberhinaus sind wir an einer statisches Analyse interessiert und trachten danach existierende Programmiersprachen behandeln zu können, nicht nur künstliche Sprachkonstrukte. In den letzten Jahren hat es vielfältige Zugänge zur automatischen Analyse von Programmkomplexität gegeben, etwa im Bereich von eingebetteten Systemen, oder in Korrektheitsbeweisen von Programmbibliotheken. Der erste Anwendungsbereich kann motiviert werden, wenn man sich ein kleines Programm vorstellt, dass auf einem Smartphone effizient funktionieren soll. Jede unnötige Resourcenverschwendung muss vermieden beziehungsweise entdeckt werden, bevor das Programm weltweit verbreitet wird. In diesem Projekt werden wir das folgende Ziel verfolgen: "Erweiterung des derzeitigen Wissensstandes zur Analyse von Programmen. Dazu werden wir automatische Laufzeitkomplexitätsanalysen betrachten, die mittels Transformationen funktionieren." Das heißt wir werden keinen direkten Zugang versuchen, sonderen mit Hilfe von Programmtransformationen vorgehen: Zuerst übersetzen wir das Eingabeprogramm in ein Termersetzungssystem und dann verwenden wir die im Rahmen des Projekes entwickelten Methoden zur (automatischen) Komplexitäts-analyse von Termersetzungsssystemen. In dieser Weise können wir den einfachen und eleganten Zugang von Termersetzungssystemen verwenden. Wir betrachten die Analogie zur SAT Technologie. Im Prinzip ist die Frage, ob eine propositionale Formel erfüllbar ist, nur von theoretischem Interesse. Nach bahnbrechenden Ergebnissen zu dieser Frage ist der derzeitige Stand der Forschung aber, dass SAT Technologie eine sehr mächtiges Arsenal für Techniken des Suchens liefert. Kaum eine ad-hoc problemspezifische Lösung liefert bessere Ergebnisse als die Verwendung von existierenden SAT Werkzeugen. Es ist unsere Vision, dass Termersetzung eine ähnliche Schlüsseltechnologie im Rahmen der Programmanalyse werden kann. Wir erwarten dass die Forschung in diesem Projekt den Stand der Forschung zur Komplexitätsanalyse von Programmen erweitern wird. Das Projekt wird den Erkenntnisstand zu automatischen Transformationmethoden deutlich verbessern, sowie neue Erkenntnisse im Bereich der Komplexitätsanalyse von Termersetzungssystemen hervorbringen. Darüberhinaus wird das Projekt im Besonderen Einfluß auf die Forschung im Bereich der amortisierten Kostenanalyse, der statischen Programmanalyse nehmen, sowie im Allgemeinen die Gebiete der impliziten Komplexitätstheorie, sowie der Beweistheorie positiv beeinflußen. Zusammmenfassend kann man sagen, dass uns dieses Projekt einen Schritt näher an eine "Knopfdruck"-Technik heranführt, die die Komplexitätsanalyse von realististen und sehr großen Programmen erlaubt.

Das ACAT Projekt beschäftigte sich mit der Verifikation von Software. Genauer wurden neue und hervorragend funktionierende Methode entwickelt, um automatisch feststellen zu können, ob ein untersuchter Softwarebaustein oder ein Computerprogramm innerhalb einer bestimmten Resourcenschranke ausgeführt werden kann. Dies ist ein überaus wichtiges Thema für die Informationstechnologie, da der Resourcenverbrauch eines Computerprogrammes gewissermaßen seine Nützlichkeit bestimmt. Wir sind hier an einer automatischen Analyse interessiert, die wie eine Knopfdruck- Technik funktioniert: Wir drücken einen Knopf und das Tool gibt uns detailliert Auskunft über den Resourcenverbrauch des Eingabeprogrammes. Darüberhinaus sind wir an einer statisches Analyse interessiert, das heißt an einer Analyse die bereits während der Entwicklungsphase der Software verwendet werden kann. Diese Analyse erweitert bestehende Methoden des Profilings von Programmen. Außerdem haben wir uns mit echten Programmen existierenden Programmiersprachen beschäftigt, um zukünftige praktische Anwendungen vorzubereiten.HauptresultateIm Rahmen des Projektes haben wir Methoden entwickelt, die es uns erlauben Computerprogramme, die in verschiedensten Anwendungsgebieten eingesetzt werden mit einer uniformen statischen Methode auf ihren Zeitaufwand und Speicherbedarf hin zu untersuchen. Dies gilt sowohl für sogenannte imperative Programme, deren Aufbau einer eindeutigen Befehlstruktur folgen, wie für deklarative Programme, die abstrakter formuliert sind und deshalb oftmals kürzer gehalten werden können. Die Hauptzahl der derzeit existierenden Software ist im imperativen Stil verfasst, allerdings existiert seit einigen Jahren ein starker Trend Richtung deklarativer Programmierung. Unsere Methoden und im Besonderen das da- rauf aufbauende Analysewerkzeug TCT sind einzigartig in ihrer universellen Anwendbarkeit. Diese Universalität zeigt sich auch deutlich in internationalen Wettbewerben, bei denen TCT immer als eines der allgemeinsten Analysewerkzeuge überzeugt. Im Rahmen der ersten FLoC Olympic Games, abgehalten im Rahmen des Vienna Summer of Logic 2014, hat TCT eine prestigeträchtig Kurt Gödel Medaille gewonnen.Methodologie Unser Ansatz zur Programmanalyse verwendet Programmtransformationen. Zuerst abstrahieren wir das Eingabeprogramm zu einem formal leicht zu beschreibenden Regelsystem (einem Termersetzungssystem), um anschließend bestehende Analysemethoden für Termersetzungssysteme verwenden zu können. Durch diese Methode können wir den einfachen und eleganten Zugang von Termersetzungssystemen verwenden. Darüberhinaus begründet dieser Zugang die universelle Anwendbarkeit von TCT.Fakten Das ACAT Projekt war ein Einzelforschungprojekt der Grundlagenforschung im Bereich der theoretischen Informatik und der Logik. Es wurde von Georg Moser koordiniert.