% IMPORTANT: The following is UTF-8 encoded. This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.
@PHDTHESIS{Brockschmidt:459458,
author = {Brockschmidt, Marc},
othercontributors = {Giesl, Jürgen},
title = {{T}ermination analysis for imperative programs operating on
the heap},
volume = {2013,18},
address = {Aachen},
publisher = {Publikationsserver der RWTH Aachen University},
reportid = {RWTH-CONV-145366},
series = {Aachener Informatik-Berichte},
pages = {II, 224 S. : graph. Darst.},
year = {2014},
note = {Prüfungsjahr: 2013. - Publikationsjahr: 2014; Zugl.:
Aachen, Techn. Hochsch., Diss., 2013},
abstract = {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.},
keywords = {Verifikation (SWD) / Programmanalyse (SWD) / Terminierung
<Informatik> (SWD)},
cin = {120000 / 121420},
ddc = {004},
cid = {$I:(DE-82)120000_20140620$ / $I:(DE-82)121420_20140620$},
shelfmark = {F.3.1 * D.2.4},
typ = {PUB:(DE-HGF)11 / PUB:(DE-HGF)3},
urn = {urn:nbn:de:hbz:82-opus-52325},
url = {https://publications.rwth-aachen.de/record/459458},
}
guest ::