TU Darmstadt / ULB / TUprints

Automatic generation of specifications using verification tools

Wasser, Nathan Daniel :
Automatic generation of specifications using verification tools.
Technische Universität Darmstadt, Darmstadt
[Ph.D. Thesis], (2017)

[img]
Preview
Text
Dissertation_Stand_20170117.pdf
Available under CC-BY-NC-ND 4.0 International - Creative Commons Attribution Non-commercial No-derivatives 4.0.

Download (1MB) | Preview
Item Type: Ph.D. Thesis
Title: Automatic generation of specifications using verification tools
Language: English
Abstract:

This dissertation deals with the automatic generation of sound specifications from a given program in the form of loop invariants and method contracts. Sound specifications are extremely useful, in that without them analysis of non-trivial programs becomes almost impossible. Verification tools can be used to prove complex properties for real-world programs, but this requires the presence of sound specifications for unbounded loops and unbounded recursive method calls. If even one simple specification is missing, the proof may become impossible to close.

In general automation and precision are two goals which are often mutually exclusive. To ensure that the generation of specifications is fully automatic, precision will suffer. Approaches exist which perform abstraction on programs, replacing all types with abstracted counterparts with only finitely many different abstract values. Thus algorithms relying on fixed points for these abstract values can be used in the automatic generation of specifications, ensuring termination thereof. Precision is lost not only at the loops and method calls where this is required to ensure automation, however, but in the entire program.

The automatic generation of specifications illustrated in this dissertation is characterized by the following: (i) abstraction is restricted to the loops and method calls themselves, ensuring that precision is kept for the remaining program, (ii) the loss of precision due to abstraction is partially reduced, by coupling the abstraction with introduction of new invariants which aim to counteract this loss of precision to a certain degree, and (iii) non-standard control flows of real-world programming languages are supported, rather than restricting the analysis to an academic toy language.

In order to restrict the loss of precision to loops and method calls, abstraction is performed on program states, rather than the entire program. This allows full precision to be kept where possible, while program states related to loops and method calls are abstracted in order to ensure the termination of fixed point algorithms. The abstraction of program states is performed using abstract domains for the corresponding types. These abstract values can then be used outside of the loop or method call as normal values for which only partial knowledge is present. Real-world programming languages, such as Java, can contain, for example, a program heap which can be modified in loops or method calls, as well as objects and arrays as types in addition to the simpler primitive types such as booleans and integers. This leads to abstract domains being presented for objects and program heaps.

As abstract domains are hard to fine-tune, additional invariants are introduced when abstracting, to counteract the coarse overapproximations. This allows abstraction of an array's elements, for example, by a coarse overapproximation of the program heap on which the elements reside, in addition to the introduction of invariants regarding the values of said array elements.

Real-world programming languages contain many elements that make the automatic generation of specifications much harder than these are on academic toy languages or strongly reduced subsets of real-world languages. Both loops and simple recursion are comparatively easy to reason about by themselves, however combining these, where a method calls itself recursively inside a loop, makes automatic generation of specifications a much harder task. Mutual recursion and non-standard control flows such as breaking out of a loop, throwing exceptions or returning from a method call while inside a loop add further complications. This dissertation describes how to automatically generate specifications in all of these cases.

Alternative Abstract:
Alternative AbstractLanguage
Diese Dissertation beschreibt die automatische Erzeugung korrekter Spezifikationen aus einem gegebenen Programm in Form von Schleifeninvarianten und Methodenverträge. Korrekte Spezifikationen sind für die Analyse nichttrivialer Programme unumgänglich. Verifikationswerkzeuge können komplexe Eigenschaften von realen Programmen beweisen, benötigen aber hierzu korrekte Spezifikationen für unbeschränkte Schleifen und unbeschränkte rekursive Methodenaufrufe. Selbst das Fehlen einer einzigen Spezifikation kann dazu führen, dass der Beweis nicht geschlossen werden kann. Im Allgemeinen sind Automatisierung und Präzision Ziele, die sich oft gegenseitig ausschließen. Die Herausforderung besteht häufig darin einen guten Mittelweg zu finden. Um vollautomatische Erzeugung von Spezifikationen zu erlangen, müssen Kompromisse bei der Präzision hingenommen werden. Es existieren Ansätze, die Programme als Ganzes abstrahieren, indem alle Typen durch abstrakte Typen ersetzt werden, die nur endlich viele abstrakte Werte beinhalten. Dies ermöglicht es bei der automatischen Spezifikationserzeugung Algorithmen zu verwenden, die auf Fixpunktberechnung beruhen, und so deren Terminierung zu garantieren. Bei den bisherigen Ansätzen tritt ein Präzisionsverlust nicht nur bei Schleifen oder Methodenaufrufen auf, bei denen dieses zum Sicherstellen der Automatisierung notwendig ist, sondern im gesamten Programm. Die in dieser Dissertation vorgestellte Spezifikationserzeugung zeichnet sich durch folgende Punkte aus: (i) Abstraktion findet nur bei Schleifen und Methodenaufrufen statt, so dass Präzision an allen anderen Stellen des Programms beibehalten wird, (ii) durch das Koppeln der Abstraktion an die Einführung neuer Invarianten wird eine präzisere Darstellung des symbolischen Programmzustandes erreicht, und (iii) werden komplexere Konstrukte zur Steuerung des Kontrollflusses realer Programmiersprachen unterstützt, anstatt sich auf einer akademischen Spielsprache zu beschränken. Um den Präzisionsverlust zu minimieren, werden Programmzustände abstrahiert, an Stelle ganzer Programme. Um die Terminierung der Fixpunktalgorithmen sicherzustellen, müssen Programmzustände bei Schleifen oder Methodenaufrufen abstrahiert werden. Die Abstraktion von Programmzuständen wird mittels abstrakter Domänen passenden Typs ausgeführt. Diese abstrakten Werte können dann ausserhalb der Schleife oder des Methodenaufrufs als normale Werte betrachtet werden, für die nur Teilwissen zur Verfügung steht. Reale Programmiersprachen wie Java beinhalten zum Beispiel sowohl einen Programm-Heap, der von Schleifen oder Methodenaufrufen verändert werden kann, als auch Objekte und Arrays als Typen neben den Primitivtypen wie Bool'sche Werte oder ganze Zahlen. Abstrakte Domänen für Objekte und Programm-Heaps werden vorgestellt. Da abstrakte Domänen sich nur schwer problemspezifisch anpassen lassen, werden zusätzliche Invarianten beim Abstrahieren eingeführt, um den Folgen der Überapproximation etwas entgegenzuarbeiten. Dies erlaubt es zum Beispiel Wissen über die Werte der Elemente eines Arrays beizubehalten, die ansonsten bei der Durchführung der Abstraktion verloren gegangen wären. Reale Programmiersprachen beinhalten viele Konstrukte, die die automatische Spezifikationserzeugung erschweren. Sowohl bei Schleifen als auch bei einfacher Rekursion ist die automatische Spezifikationserzeugung vergleichsweise einfach zu realisieren. Kompliziertere Fälle, wie zum Beispiel wechselseitige Rekursion, stellen die automatische Spezifikationserzeugung vor signifikant größere Herausforderungen. Auch nichtstandard Kontrollflüsse, wie das Verlassen einer Schleife durch ein break, das Werfen einer Exception oder das Verlassen einer Methode innerhalb einer Schleife, sind weitere Komplikationen bei der automatischen Spezifikationserzeugung. Das in dieser Dissertation entwickelte Verfahren kann für alle diese Fälle korrekte Spezifikationen automatisch erzeugen.German
Place of Publication: Darmstadt
Classification DDC: 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Divisions: 20 Department of Computer Science > Software Engineering
Date Deposited: 30 Jan 2017 14:31
Last Modified: 14 Feb 2017 09:32
URN: urn:nbn:de:tuda-tuprints-59109
Referees: Hähnle, Prof. Dr. Reiner and Kovacs, Prof. Dr. Laura
Refereed: 26 February 2016
URI: http://tuprints.ulb.tu-darmstadt.de/id/eprint/5910
Export:
Actions (login required)
View Item View Item

Downloads

Downloads per month over past year