h1

000459458 001__ 459458
000459458 005__ 20250613102914.0
000459458 0247_ $$2ISSN$$a0935-3232
000459458 0247_ $$2URN$$aurn:nbn:de:hbz:82-opus-52325
000459458 0247_ $$2HSB$$a1999910014870
000459458 0247_ $$2OPUS$$a5232
000459458 0247_ $$2Laufende Nummer$$a33643
000459458 037__ $$aRWTH-CONV-145366
000459458 041__ $$aEnglish
000459458 082__ $$a004
000459458 0847_ $$2ccs$$aF.3.1 * D.2.4
000459458 1001_ $$0P:(DE-82)057842$$aBrockschmidt, Marc$$b0$$eAuthor
000459458 245__ $$aTermination analysis for imperative programs operating on the heap$$cMarc Brockschmidt$$honline, print
000459458 246_3 $$aTerminierungsanalyse imperativer Programme mit Heapoperationen$$yGerman
000459458 260__ $$aAachen$$bPublikationsserver der RWTH Aachen University$$c2014
000459458 300__ $$aII, 224 S. : graph. Darst.
000459458 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
000459458 3367_ $$02$$2EndNote$$aThesis
000459458 3367_ $$2DRIVER$$adoctoralThesis
000459458 3367_ $$2BibTeX$$aPHDTHESIS
000459458 3367_ $$2DataCite$$aOutput Types/Dissertation
000459458 3367_ $$2ORCID$$aDISSERTATION
000459458 3367_ $$0PUB:(DE-HGF)3$$2PUB:(DE-HGF)$$aBook$$mbook
000459458 4900_ $$aAachener Informatik-Berichte$$v2013,18
000459458 4900_ $$aTechnical report / Department of Computer Science, RWTH Aachen
000459458 500__ $$aPrüfungsjahr: 2013. - Publikationsjahr: 2014
000459458 502__ $$aZugl.: Aachen, Techn. Hochsch., Diss., 2013$$gFak01$$o2013-11-19
000459458 5203_ $$aDie 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.$$lger
000459458 520__ $$aAnalysing 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.$$leng
000459458 591__ $$aGermany
000459458 650_7 $$2SWD$$aVerifikation
000459458 650_7 $$2SWD$$aProgrammanalyse
000459458 650_7 $$2SWD$$aTerminierung <Informatik>
000459458 653_7 $$aInformatik
000459458 653_7 $$2eng$$averification
000459458 653_7 $$2eng$$aprogram analysis
000459458 653_7 $$2eng$$atermination analysis
000459458 7001_ $$0P:(DE-82)IDM00052$$aGiesl, Jürgen$$b1$$eThesis advisor
000459458 8564_ $$uhttps://publications.rwth-aachen.de/record/459458/files/5232.pdf
000459458 909CO $$ooai:publications.rwth-aachen.de:459458$$pdnbdelivery$$popenaire$$popen_access$$purn$$pdriver$$pVDB
000459458 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
000459458 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x0
000459458 9201_ $$0I:(DE-82)121420_20140620$$k121420$$lLehr- und Forschungsgebiet Informatik 2 (Programmiersprachen und Verifikation)$$x1
000459458 961__ $$c2015-01-05$$x2014-12-22$$z2012-02-20
000459458 970__ $$aHT018447785
000459458 9801_ $$aFullTexts
000459458 980__ $$aphd
000459458 980__ $$aI:(DE-82)120000_20140620
000459458 980__ $$aI:(DE-82)121420_20140620
000459458 980__ $$aVDB
000459458 980__ $$aUNRESTRICTED
000459458 980__ $$aConvertedRecord
000459458 980__ $$abook