Holonome Folgen in der Programmverifikation

Wer sich in die Abhängigkeit komplexer Softwaresysteme begibt im Flugzeug, im Krankenhaus oder im Auto muss darauf vertrauen können, dass die beteiligten Programme ihre Aufgaben fehlerfrei verrichten. Um dies sicherzustellen, werden im Bereich der automatisierten Programmanalyse und -verifikation computergestützte formale Beweise erzeugt, die die Korrekheit der verwendeten Algorithmen mit mathematischen Mitteln belegen. Ein wesentlicher Bestandteil der Programmanalyse ist die Charakterisierung der möglichen Daten, die während der Programmausführung in Variablen gespeichert, manipuliert und weiterverarbeitet werden. Dies kann mit Hilfe von Gleichungen und Ungleichungen geschehen, welche die Grenzen für den erreichbaren Wertebereich der Daten beschreiben. Kann eine Variable in dem zu analysierenden Algorithmus negative Werte annehmen? Ergibt die Summe der Werte zweier Variablen jemals die Zahl Null? Antworten auf derartige Fragen sind notwendig zur Vermeidung von auf Programmfehlern basierender Unfälle, wie etwa der Explosion der unbemannten Ariane 5 Rakete im Jahre 1994. Gleichzeitig gehört die Suche nach ihnen jedoch zu den schwierigsten Problemen in der Programmanalyse. Unser Ziel ist es, algorithmische Methoden zur automatisierten Suche nach passenden Gleichungen und Ungleichungen zu entwickeln, basierend auf Techniken aus dem Bereich der Computeralgebra und der statischen Programmanalyse. Werte von Variablen ändern sich nicht willkürlich, sondern bilden regelmäßige Zahlenfolgen. In der überwiegenden Mehrheit von Programmen fallen diese Zahlenfolgen in die Klasse der holonomen Folgen, welche auch die prominente Fibonacci-Folge enthält. Die mathematische Theorie holonomer Folgen hat bereits zahlreiche Verfahren zu deren Analyse hervorgebracht, die jedoch selbst in einigen vermeintlich einfachen Fällen ungenügend sind. Darüber hinaus fanden diese Verfahren bislang nur vereinzelt Anwendung in der automatisierten Programmverifikation. In diesem Projekt erforschen wir Möglichkeiten, Techniken aus den Bereichen der Programmanalyse und der Mathematik holonomer Folgen zu kombinieren um Theorie und Praxis in beiden Forschungsbereichen voranzubringen. So arbeiten wir zum einen daran, die für die Analyse von Folgen entwickelten Methoden für den gezielten Einsatz in der Programmanalyse anzupassen. Dadurch kann die Abgrenzung von Wertebereichen von Variablen noch präziser und effektiver durchgeführt werden. Zum anderen untersuchen wir, wie offene Fragen holonome Folgen betreffend durch neue und bestehende Techniken der Programmverifikation beantwortet werden können. Wir erhalten dadurch neue Einsichten in die mathematische Theorie die diesen Folgen zugrunde liegt und ermöglichen zudem Forschern und Anwendern computergestützter Mathematik Zugriff auf leistungsfähige Verfahren zur Handhabung von Folgen und Ungleichungen.

Das Projekt "Holonome Folgen in der Programmverifikation" beschäftigte sich mit der automatisierten mathematischen Analyse von Algorithmen, welche heute in zahllosen Computerprogrammen in allen Bereichen des täglichen Lebens verwendet werden. Eine solche Analyse ermöglicht es, das korrekte Verhalten der Programme zu belegen, was vor allem in sicherheitskritischen Anwendungsdomänen von höchster Wichtigkeit ist. Trotz großer Anstrengungen, welche bis zum Beginn des 20. Jahrhunderts und der ersten Formulierung des modernen Verständnisses des Begriffs "Computer" zurückreichen, hat die automatisierte Programmanalyse ihren Status eines fundamentalen und nur in wenigen Spezialfällen effizient zu lösenden Problems nicht eingebüßt. Mit einem innovativen Ansatz machten es sich die Forscher in diesem Projekt zum Ziel, mit Hilfe zahlreicher Theorien aus dem Werkzeugkasten der Mathematik neue Wege zur Lösung dieses Problems zu erkunden. Durch die Zusammenführung moderner Ergebnisse, unter anderem aus den Bereichen der diskreten Mathematik, der Computeralgebra und der algorithmischen Geometrie, konnten sie wertvolle neue Kenntnisse erarbeiten, welche sich in Zukunft bei der Suche nach neuen Methoden der Programmverifikation als fundamentaler Beitrag erweisen könnten. Zusätzlich zu der Erarbeitung theoretischer Ergebnisse wurden in diesem Projekt auch die Rahmenbedingungen für zielgerichtete Experimente für weiterführende Forschung geschaffen. Dies geschah in Form einer Sammlung von Programmen - in der Informatik "Bibliothek" genannt - welche eine detaillierte Analyse von Systemen von Differential- und Differenzengleichungen erlaubt. Solche Gleichungssysteme sind die zentralen Objekte in der mathematischen Repräsentation komplexer Phänomene, unter anderem auch in der Modellierung der Änderungen von gespeicherten Daten während der Ausführung von Computerprogrammen. Die Bibliothek steht interessierten Benutzern kostenfrei und mit frei zugänglichem Quellcode zur Verfügung. Obwohl die Forschungsarbeit in den letzten 12 Monaten des Projekts durch den Ausbruch der Corona-Pandemie und der daraus resultierenden, notwendigen Beschränkungen stark beeinflusst wurden, ist es den beteiligten Wissenschaftlern gelungen, die wissenschaftliche Gemeinschaft mit wichtigen Beiträgen zu unterstützen, und den Stellenwert der Grundlagenforschung in Österreich weiter zu stärken.