Termination of rewriting and its certification

A. Koprowski

    Onderzoeksoutput: ScriptieDissertatie 1 (Onderzoek TU/e / Promotie TU/e)

    177 Downloads (Pure)


    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.
    Originele taal-2Engels
    KwalificatieDoctor in de Filosofie
    Toekennende instantie
    • Mathematics and Computer Science
    • Zantema, Hans, Promotor
    • Groote, Jan Friso, Promotor
    Datum van toekenning25 sep 2008
    Plaats van publicatieEindhoven
    Gedrukte ISBN's978-90-386-1377-2
    StatusGepubliceerd - 2008


    Duik in de onderzoeksthema's van 'Termination of rewriting and its certification'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit