Termination analysis for imperative programs operating on the heap

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