Combining norms to prove termination

S. Genaim, M. Codish, John Patrick Gallagher, V. Lagoon

    Research output: Chapter in Book/Report/Conference proceedingBook chapterResearch

    Abstract

    Automatic termination analysers typically measure the size of terms applying norms which are mappings from terms to the natural numbers. This paper illustrates howt o enable the use of size functions defined as tuples of these simpler norm functions. This approach enables us to simplify the problem of deriving automatically a candidate norm with which to prove termination. Instead of deriving a single, complex norm function, it is sufficient to determine a collection of simpler norms, some combination of which, leads to a proof of termination. We propose that a collection of simple norms, one for each of the recursive data-types in the program, is often a suitable choice. We first demonstrate the power of combining norm functions and then the adequacy of combining norms based on regular types.
    Original languageEnglish
    Title of host publicationVerification, model checking, and abstract interpretation, Third International Workshop, VMCAI 2002 : Venice, Italy, January 21-22, 2002
    EditorsAgostino Cortesi
    PublisherSpringer
    Publication date2002
    Pages126-138
    ISBN (Print)3-540-43631-6
    Publication statusPublished - 2002
    SeriesLecture Notes in Computer Science
    Volume2294
    ISSN0302-9743

    Cite this