Towards complete methods for automatic complexity and termination analysis of (probabilistic) programs

• Methoden für die automatische Komplexitäts- und Terminierungsanalyse von (probabilistischen) Programmen und ihre Vollständigkeit

Hark, Marcel Tobias; Giesl, Jürgen (Thesis advisor); Kovács, Laura (Thesis advisor)

Aachen : RWTH Aachen University (2021)
Doktorarbeit

Dissertation, RWTH Aachen University, 2021

Kurzfassung

Die steigende Zahl von Computerprogrammen in unserem Alltag hat zu immer umfangreicheren Softwaresystemen geführt. Die klassische Herangehensweise, um die Korrektheit solcher Systeme zu garantieren, ist formale Verifikation. Zwei der wichtigsten Eigenschaften von Programmen sind Terminierung und Effizienz. Außerdem wird in den letzten Jahren Randomisierung in der Programmierung immer wichtiger. So haben probabilistische Konzepte sich als sehr erfolgreich erwiesen, um Systeme aus praxisnahen Anwendungen zu modellieren. Diese Dissertation untersucht die formale Verifikation von Programmen, welche auch randomisierte Zuweisungen durch diskrete Zufallsverteilungen unterstützen. Hierbei sind wir besonders daran interessiert, Terminierung bzw. Nichtterminierung zu beweisen und Schranken für die (erwartete) Laufzeit zu berechnen. Verifikation von Programmen ist im Allgemeinen unentscheidbar. Dennoch sind wann immer möglich vollständige Ansätze zur Verifikation bestimmter Eigenschaften von (Teil-)Klassen von Programmen unvollständigen vorzuziehen, da sie immer ein eindeutiges Ergebnis liefern, also entweder einen Beweis oder ein Gegenbeispiel. Ein wichtiges Ziel dieser Arbeit ist daher die Charakterisierung von Teilklassen von Programmen, für die vollständige Techniken zur Analyse von Terminierung und Laufzeitkomplexität existieren. Um Systeme zu analysieren, die aus praxisnahen Anwendungen hervorgehen, muss formale Verifikation automatisch ablaufen. Daher studieren wir auch die Automatisierung der hier vorgestellten Techniken. Die Beiträge dieser Arbeit sind im Folgenden aufgelistet. (1) Wir beschreiben Klassen nicht-probabilistischer Programme, für die sowohl Terminierung auf einer gegebenen Eingabe als auch Terminierung auf allen Eingaben entscheidbar sind, nichtterminierende Eingaben rekursiv aufgezählt und obere Schranken für die Laufzeit immer berechnet werden können. (2) Wir verknüpfen die Semantik probabilistischer Programme, die durch sogenannte Erwartungs-Kalküle gegeben ist, mit jener, die durch sogenannte stochastische Prozesse definiert ist. So erhalten wir die ersten induktiven Beweisregeln zur Bestimmung unterer Schranken für die erwarteten Ausgaben bzw. Laufzeiten probabilistischer Programme. (3) Wir präsentieren eine Klasse probabilistischer Programme, für welche nicht nur Terminierung entscheidbar ist und sowohl obere als auch untere Schranken für die erwartete Laufzeit leicht hergeleitet werden können, sondern auch eine geschlossene Form für die exakte erwartete Laufzeit immer berechnet werden kann. (4) Wir entwickeln einen Ansatz zur Bestimmung oberer Schranken für die erwartete Laufzeit allgemeiner probabilistischer Programme. Hierfür benutzen wir sowohl Schranken für die klassische Laufzeit bzw. Größe von Variablenwerten als auch eine abwechselnde Berechnung von Schranken für die erwartete Laufzeit bzw. Größe. Unsere experimentelle Auswertung zeigt die große Leistungsfähigkeit dieses Ansatzes.