Direkt zum Inhalt | Direkt zur Navigation

Eingang zum Volltext

Lizenz

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:bsz:25-opus-69727
URL: http://www.freidok.uni-freiburg.de/volltexte/6972/


Wies, Thomas

Symbolic shape analysis

Symbolische Shape-Analyse

Dokument1.pdf (1.008 KB) (md5sum: bcf1c82b2d69b6055c5c659e7ccc52c1)

Kurzfassung in Deutsch

Programmverifikation stellt die Zuverlässigkeit von Software sicher, indem sie einen mathematischen Beweis erbringt, der die Korrektheit der Software garantiert. Werkzeuge zur Programmverifikation unterstützen den Entwickler bei diesem Verifikationsprozess. Idealerweise sollte solch ein Werkzeug auf eine
Vielzahl von Verifikationsproblemen anwendbar sein, ohne dass es eine hohe Bürde für dessen Benutzer darstellt, d.h. ohne tiefgreifende mathematische Kenntnisse und Erfahrung in der Programmverifikation vorauszusetzen.

Ein großer Schritt diesem Ideal nahezukommen wurde durch die Kombination der Methode der "abstrakten Interpretation" und Techniken des "automatischen Theorembeweisens" erzielt. In der abstrakten Interpretation transformiert man das "konkrete" Programm in ein "abstraktes" Programm. Das abstrakte Programm
ermöglicht eine Programmanalyse, die statische Informationen über alle Ausführungen des konkreten Programms sammelt. Die gesammelten Informationen werden dann dazu verwendet die Korrektheit des konkreten Programms automatisch zu beweisen. Die abstrakte Interpretation erhöht den Automatisierungsgrad in der Verifikation, indem sie die Bürde der formalen Beweisführung über Programme vom Softwareentwickler an den Designer der Programmanalyse delegiert. Durch Techniken des automatischen Theorembeweisens lässt sich der Automatisierungsgrad noch weiter erhöhen. Diese Techniken ermöglichen die automatische Konstruktion der Abstraktion für ein spezifisches Programm und eine spezifische Korrektheitseigenschaft und (falls nötig) auch die automatische Verfeinerung dieser Abstraktion. Wir bezeichnen Programmanalysen, die abstrakte Interpretation mit automatischem Theorembeweisen verbinden, als "symbolische" Programmanalysen.

Ein Problem, dem in jüngster Zeit viel Beachtung geschenkt wird, ist die Fragestellung, wie man in der Verifikation und Programmanalyse effektiv mit dynamisch allozierten Zeigerstrukturen umgehen kann. Programmanalysen, deren Hauptaufgabe in der Verifikation von Eigenschaften solcher Zeigerstrukturen besteht, werden im allgemeinen als "Shape-Analysen" bezeichnet. Eine symbolische Shape-Analyse verspricht ein Spektrum verschiedener dynamisch allozierter Zeigerstrukturen und ein Spektrum an Eigenschaften verifizieren zu
können, ohne dass der Benutzer die Analyse manuell an eine spezifische Probleminstanz anpassen muss. Die Frage, wie solch eine symbolische Shape-Analyse aussehen könnte und ob sie den an sie gestellten Erwartungen gerecht würde, war offen. In der vorliegenden Dissertation beschäftigen wir uns mit dieser Frage.

Wir stellen die "universelle Prädikatenabstraktion" vor, die die Methode der Prädikatenabstraktion bis zu dem Punkt verallgemeinert, an dem sie sich effektiv als Shape-Analyse einsetzen lässt. Die universellen Prädikatenabstraktion resultiert aus der Übertragung der Schlüsselidee der dreiwertigen Shape-Analyse nach Sagiv, Reps, und Wilhelm in die Prädikatenabstraktion, indem wir Prädikate über Programmzuständen durch Prädikate über Objekte im Heap von Programmzuständen ersetzten. Wir zeigen wie man die Transformation eines Zeigerprogramms in ein abstraktes Programm durch die Verwendung automatischer Theorembeweiser automatisieren lässt. Des weiteren
entwickeln wir eine Methode zur automatischen Abstraktionsverfeinerung, die die universelle Prädikatenabstraktion zu einer vollautomatischen symbolischen Shape-Analyse ergänzt. Schließlich stellen wir die Methode der "Feldbedingungsanalyse" vor, einer neuen automatischen Beweisführungsmethode für Zeigerprogramme. Die Feldbedingungsanalyse ermöglicht die Anwendung von Entscheidungsprozeduren zur Beweisführung über spezifische Datenstrukturen (wie z.B. Bäume) auf beliebige Datenstrukturen. Diese Technik macht unsere symbolische Shape-Analyse auf die vielfältigen Datenstrukturen anwendbar, die in der Praxis auftreten.

Alle Techniken, die in dieser Dissertation vorgestellt werden, haben wir im Verifikationswerkzeug Bohne implementiert und evaluiert. Wir haben Bohne dazu verwendet komplexe benutzerspezifizierte Eigenschaften von Datenstrukturimplementierungen zu verifizieren. Insbesondere waren wir in der Lage die Erhaltung von Konsistenzeigenschaften für Operationen auf geketteten Binärbäumen zu verifizieren (darunter Sortiertheit und die Inorder-Traversierungseigenschaft). Dies gelang ohne unsere Analyse speziell für dieses Problem anzupassen und ohne jegliche Hilfe des Benutzers, die über die bloße Formulierung der zu beweisenden Eigenschaften hinausginge. Uns ist keine andere Shape-Analyse bekannt, die diese Eigenschaften mit einem vergleichbaren Automatisierungsgrad verifizieren könnte.


Kurzfassung in Englisch

The goal of program verification is to ensure software reliability by establishing a mathematical proof which guarantees that the software behaves correctly. Program analysis tools assist the developer in the verification process. Ideally a program analysis should be applicable to a wide range of verification problems without imposing a high burden on its users, i.e., without requiring deep mathematical knowledge and experience in program verification.

A big step forward towards this ideal has been achieved by combining "abstract interpretation" with techniques for "automated reasoning". In abstract interpretation one transforms the "concrete program" into an "abstract program". The abstract program enables the analysis to statically collect information over all possible executions of the concrete program. This information is used to automatically verify the correctness of the concrete program. Abstract interpretation increases the degree of automation in verification by shifting the burden of formally reasoning about programs from the developer to the designer of the program analysis. Automated reasoning pushes the degree of automation even further. It enables the automatic construction of the abstraction for a specific program and a specific correctness property and (if necessary) the automatic refinement of this abstraction. We refer to program analyses that combine abstract interpretation with automated reasoning as "symbolic program analysis".

A problem that has recently seen much attention in program verification is the question of how to effectively deal with linked heap-allocated data structures. Program analyses that target properties of these data structures are commonly referred to as "shape analyses". A symbolic shape analysis promises to handle a spectrum of different linked heap-allocated data structures, and a spectrum of properties to verify, without requiring the user to manually adjust the analysis to the specific problem instance. It was open what a symbolic shape analysis would look like. In this thesis we are concerned with this question.

We present "domain predicate abstraction", which generalizes predicate abstraction to the point where it becomes effectively applicable for shape analysis. Domain predicate abstraction incorporates the key idea of three-valued shape analysis into predicate abstraction by replacing predicates on program states by predicates on objects in the heap of program states. We show how to automate the transformation of a heap-manipulating program into an abstract program using automated reasoning procedures. We further develop an abstraction refinement technique that complements domain predicate abstraction to a fully automated symbolic shape analysis. Finally, we present "field constraint analysis", a new technique for reasoning about heap programs. Field constraint analysis enables the application of decision procedures for reasoning about specific data structures (such as trees) to arbitrary data structures. This technique makes our symbolic shape analysis applicable to the diverse data structures that occur in practice.

All the techniques presented in this thesis have been implemented and evaluated in the Bohne Verifier. We used Bohne to verify complex user-specified properties of data structure implementations. For instance, we were able to verify preservation of data structure invariants for operations on threaded binary trees (including sortedness and the in-order traversal invariant) without manually adjusting the analysis to this specific problem or providing user assistance beyond stating the properties to verify. We are not aware of any other shape analysis that can verify such properties with a comparable degree of automation.


SWD-Schlagwörter: Programmanalyse , Verifikation
Freie Schlagwörter (deutsch): Datenstrukturen, Zeigerprogramme
Freie Schlagwörter (englisch): Verification, Program Analysis, Data Structures, Heap Programs
CCS Klassifikation F.3.2 , F.3.1 , D.2.4
Institut: Institut für Informatik
Fakultät: Technische Fakultät (bisher: Fak. f. Angew. Wiss.)
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Erstgutachter: Podelski, Andreas (Prof. Dr.)
Sprache: Englisch
Tag der mündlichen Prüfung: 09.11.2009
Erstellungsjahr: 2009
Publikationsdatum: 16.11.2009
Indexliste