Automatic Termination Analysis for Functional and Imperative Programs

Verifying the termination of algorithms is a central problem in computer science. In this thesis we present a new method for automating termination proofs for functional and imperative programs. In our approach, an imperative program is translated into an equivalent functional one whose termination is analyzed instead. In general, this translation yields recursive sub-procedures which terminate only partially, i.e., if their inputs satisfy certain preconditions. However, previous methods for functional programs try to prove that each procedure terminates totally, i.e., for each input. We present the first approach to analyzing the termination behavior of partially terminating procedures by machine. Our proposal generalizes earlier work and provides a method for proving termination of several functional and imperative programs without human interaction.