Automatic Termination Analysis for Functional and Imperative Programs

Share
Author
Brauburger, J.
Pub. date
January 1999
Pages
244
Binding
softcover
Volume
207 of Dissertations in Artificial Intelligence
ISBN print
978-1-58603-113-8
Subject
Artificial Intelligence, Computer & Communication Sciences, Computer Science

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.