Termination analysis for imperative programs operating on the heap

Brockschmidt, Marc; Giesl, Jürgen

doi:5232

Termination analysis for imperative programs operating on the heap = Terminierungsanalyse imperativer Programme mit Heapoperationen

Brockschmidt, Marc (Author)

2014

VerantwortlichkeitsangabeMarc Brockschmidt

ImpressumAachen : Publikationsserver der RWTH Aachen University 2014

UmfangII, 224 S. : graph. Darst.

ReiheAachener Informatik-Berichte Technical report / Department of Computer Science, RWTH Aachen ; 2013,18

Zugl.: Aachen, Techn. Hochsch., Diss., 2013

Prüfungsjahr: 2013. - Publikationsjahr: 2014

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Giesl, Jürgen (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2013-11-19

Online
URN: urn:nbn:de:hbz:82-opus-52325
URL: https://publications.rwth-aachen.de/record/459458/files/5232.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Verifikation (Genormte SW) ; Programmanalyse (Genormte SW) ; Terminierung <Informatik> (Genormte SW) ; Informatik (frei) ; verification (frei) ; program analysis (frei) ; termination analysis (frei)

Thematische Einordnung (Klassifikation)
DDC: 004
ccs: F.3.1 * D.2.4

Kurzfassung
Die Terminierungsanalyse von Programmen und Prozessen ist eines der zentralen Themen der theoretischen Informatik. Obwohl bekannt ist, dass das Problem im Allgemeinen unentscheidbar ist, wird es seit Jahrzehnten untersucht. Hierbei wurden zahlreiche Techniken entwickelt, um die Terminierung von kleinen Beispielprogrammen zu beweisen. Basierend auf diesen grundlegenden Resultaten hat sich der Fokus der Forschung nun auf die Terminierungsanalyse von praktisch verwendeten Programmen verschoben. Zwei verschiedene Ansätze für die Terminierungsanalyse weit verbreiteter Programme wurden im letzten Jahrzehnt verfolgt. Ein Ansatz ist die Transformation von Programmen in theoretische Formalismen, deren Terminierungsanalyse in der Vergangenheit intensiv untersucht wurde. Auf diese Weise lassen sich direkt existierende Methoden für diese Methoden anwenden. Ein weiterer Ansatz ist das Verwenden von Techniken aus dem verwandten Gebiet der Programmverifikation, um ausgewählte Methoden für die Terminierungsanalyse einzusetzen. Diese Dissertation stellt neue Beiträge zu beiden Ansätzen vor. Zuerst wird eine Trans formation von Java Bytecode-Programmen in Termersetzungssysteme vorgestellt. Termersetzung ist ein einfacher Formalismus, der seit langem in der Terminierungsanalyse verwendet wird. Benutzerdefinierte Datenstrukturen werden dabei in Terme übersetzt. In einem zweiten Schritt werden Techniken vorgestellt, die Termersetzungssysteme mit vordefinierten ganzen Zahlen und ihren Operationen unterstützen. Mittels geeigneter Transformationen wird eine effektive Terminierungsanalyse aus spezialisierten Methoden zusammengesetzt, die entweder nur mit Termen oder nur mit ganzen Zahlen umgehen können. Schließlich werden die vorgestellten Techniken um Analysen zum Nachweis von Nichtterminierung erweitert. Um die Ansätze aus der Programmverifikation für die Terminierung von reinen Integer-Programmen zu verbessern, wird ein neues, kooperatives Beweisverfahren vorgestellt. Dessen neuartige Struktur erlaubt eine bessere Zusammenarbeit der Techniken aus der Programmverifikation und der Terminierungsanalyse. Dieses Verfahren stellt einen ersten Schritt zur Zusammenführung dieser verschiedenen Ansätze dar und erlaubt eine weitere Integration der bisher entwickelten Techniken. Basierend auf dem neuen Beweisverfahren wird außerdem ein Verfahren vorgestellt, in dem Terminierung- und Nichtterminierungsbeweise abwechseln, um weitere Programme untersuchen zu können. Die Beiträge dieser Dissertationen wurden in den vollautomatischen Terminierungsbeweisern AProVE und T2 implementiert. In der jährlichen “International Termination Competition” hat sich gezeigt, dass AProVE das mächtigste Werkzeug zur Analyse von Java Bytecode-Programmen ist, während T2 das mächtigste Werkzeug zur Terminierungsanalyse von Integer-Programmen ist.

Analysing if programs and processes terminate is one of the central topics of theoretical computer science. Even though to be undecidable in general, the problem has been studied for decades for specific subproblems. Based on the results of this work, many small example programs can be proven terminating automatically now. However, even small real-world systems usually cannot be handled. The focus has thus now turned towards proving termination of programs that are in wide-spread use in common devices and computers. Two different approaches to apply termination analysis to real-world problems have seen considerable activity in the past decade. One idea is to transform programs into formalisms that have been studied in the past, allowing to directly use existing methods and tools. Another trend is to leverage tools for model checking from the related field of safety verification to apply certain selected techniques for termination proving. This thesis makes contributions in both of these areas. First, we discuss how to transform real-world Java Bytecode programs into term rewriting, a simple formalism that has been used to study termination analysis for decades. User-defined data structures are transformed into terms, allowing to make use of the many methods originally developed for term rewriting. Then, we present techniques to handle term rewrite systems that provide pre-defined support for integers. For this, we show how using suitable transformations, a powerful termination analysis can be implemented by recursing to existing, more specialised method handling either integers or terms. Finally, we present SMT-based techniques to infer non-termination of Java Bytecode and term rewriting with integers. To improve model-checking-based approaches to termination analysis of programs restricted to integers, we present a new cooperative proof framework. Its novel structure allows model checking techniques and advanced termination proving techniques from term rewriting to work together. This work can be seen as a first step towards unifying these two approaches, and allows further cross-fertilisation of ideas. Based on this framework, we show how this approach can be used in alternation with non-termination techniques, further improving the precision of the overall approach. The contributions of this thesis are implemented in the fully automated termination prover AProVE and the model checker and termination prover T2. In the annual International Termination Competition, AProVE has proven to be the most powerful termination analyser for Java Bytecode programs, whereas T2 is the most powerful termination analyser for integer programs.

Fulltext:
PDF