Abstract
In programming, termination of a program/algorithm means that its evaluation
will eventually terminate, regardless of the input it receives. It is an important
property and is required for total correctness. In general the problem is undecid-
able.
Term rewriting is a formal way of specifying computation and as such it can be
seen as a generic model for programming languages. Termination, here meaning
lack of infinite sequences, is a well-studied concept in this context. There exist a
number of methods for proving termination as well as a number of tools for doing
that automatically. There is an on-going work on application of this methodology
and tools to proving termination of programs in actual programming languages.
In this thesis we first give a short introduction to term rewriting and to termination
of rewriting. Subsequently we present a number of contributions to this field, which
can be categorized into the following categories:
proposing new methods for proving termination and refining the existing
ones,
developing a tool for proving termination and
proposing a methodology and tools for certification of termination proofs,
i.e., formal verification of proofs produced by the existing tools for proving
termination.
Original language | English |
---|---|
Qualification | Doctor of Philosophy |
Awarding Institution |
|
Supervisors/Advisors |
|
Award date | 25 Sept 2008 |
Place of Publication | Eindhoven |
Publisher | |
Print ISBNs | 978-90-386-1377-2 |
DOIs | |
Publication status | Published - 2008 |