[Back]

F. Zuleger:
"Resource bound analysis of imperative programs";
Supervisor, Reviewer: H. Veith, S. Gulwani; Institut für Informationssysteme, 2011; oral examination: 2011-05-11.

For many practical applications it is important to bound the resources consumed by a program such as time, memory, network-traffic, power, and to estimate quantitative properties of data in programs, such as information leakage or uncertainty propagation. At the heart of many of these questions lies the problem of finding a symbolic worst-case bound on the number of visits to a given program location in terms of the inputs to that program; we call this the reachability-bound problem.
We propose a two-step methodology for computing a reachability-bound of a given program location: First, we generate a transition system that disjunctively summarizes all pairs of states for which there is a program execution that visits the location once and again. Second, we compute a bound of the transition system. We present two approaches that implement this methodology.
Our first approach brings together an abstract-interpretation based iterative technique for computing disjunctive loop invariants and a non-iterative proof-rules based technique for loop bound computation. We evaluate the effectiveness of this approach on a .Net base-class library and further benchmark programs.
Our second approach is based on the so-called size-change abstraction (SCA). We use a closure property of SCA for computing disjunctive loop invariants. We show that SCA offers a separation of concerns for bound computation: we extract local progress measures from small program parts, and then compose these local progress measures to a global bound.
We state two program transformations that make imperative programs amenable to bound analysis with SCA. We evaluate the effectiveness of this approach on two C benchmarks.
We further present results towards a theoretical characterization of the bounds expressible by SCA.
Finally we show that our solution to the reachability-bound problem captures the essential ideas of earlier termination and bound analyses and goes beyond in a simpler framework.

In vielen praktischen Anwendungen benötigt man eine Beschränkung der von Computerprogrammen verbrauchten Resourcen (z.B. Ausführungszeit, Speicher, Netzwerkverkehr, Energie) und eine Abschätzung von quantitativen Programmeigenschaften (z.B. des Verlusts geheimer Informationen oder der Ausbreitung von Fehlern). Viele dieser Fragen lassen sich auf das Problem der Berechnung einer symbolischen Schranke zurückführen, wie oft ein bestimmter Programmpunkt in Abhängigkeit von den Programmeingaben besucht werden kann; wir nennen dies das Erreichbarkeitsschrankenproblem.
Die in dieser Dissertation vorgestellte Methode berechnet eine Erreichbarkeitsschranke eines gegebenen Programmpunktes in zwei Schritten:
Im ersten Schritt erzeugen wir ein Transitionssystem, das disjunktiv alle Paare von Zuständen zusammenfasst, für die es eine Programmausführung gibt, die den Programmpunkt mindestens zweimal besucht. Im zweiten Schritt berechnen wir eine Schranke für das Transitionssystem. Wir präsentieren zwei Ansätze, die unsere Methode praktisch umsetzen.
Unser erster Ansatz verwendet eine auf abstrakter Interpretation basierende iterative Technik zur Berechnung disjunktiver Schleifeninvarianten und eine nicht-iterative auf Beweisregeln basierende Technik für die Berechnung von Schranken. Wir evaluieren die Effizienz unseres Ansatzes an einer .Net Bibliothek und weiteren Benchmark Programmen.
Unser zweiter Ansatz basiert auf der sogenannten size-change Abstraktion (SCA), die das monotone Verhalten numerischer Größen über den Programmzuständen beschreibt. Wir nützen eine Abschlusseigenschaft von SCA zur Berechnung disjunktiver Schleifeninvarianten. Mit Hilfe von SCA können wir Schranken stufenweise berechnen: Zunächst extrahieren wir lokale Fortschrittsmaße aus kleinen Programmabschnitten und setzen diese dann zu einer global gültigen Schranke zusammen. Durch zwei geeignete Programmtransformationen ermöglichen wir die Schrankenanalyse imperativer Programme. Wir evaluieren die Effizienz unserer Ansatzes anhand zweier Benchmarks für die Sprache C.
Im Anschluss präsentieren wir theoretische Beiträge, die auf eine mathematische Charakterisierung jener Schranken, die mit SCA ausgedrückt werden können, hinarbeiten. Zusammenfassend diskutieren wir, wie unser Lösungsansatz des Erreichbarkeitsschrankenproblems auf den wesentlichen Ideen früherer Terminations- und Schleifenanalysen aufbaut und diese verbessert.

https://publik.tuwien.ac.at/files/publik_196902.pdf