Combining norms to prove termination

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

    Publikation: Bidrag til bog/antologi/rapportBidrag til bog/antologiForskning

    Resumé

    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.
    OriginalsprogEngelsk
    TitelVerification, model checking, and abstract interpretation, Third International Workshop, VMCAI 2002 : Venice, Italy, January 21-22, 2002
    RedaktørerAgostino Cortesi
    ForlagSpringer
    Publikationsdato2002
    Sider126-138
    ISBN (Trykt)3-540-43631-6
    StatusUdgivet - 2002
    NavnLecture Notes in Computer Science
    Vol/bind2294
    ISSN0302-9743

    Citer dette

    Genaim, S., Codish, M., Gallagher, J. P., & Lagoon, V. (2002). Combining norms to prove termination. I A. Cortesi (red.), Verification, model checking, and abstract interpretation, Third International Workshop, VMCAI 2002: Venice, Italy, January 21-22, 2002 (s. 126-138). Springer. Lecture Notes in Computer Science, Bind. 2294
    Genaim, S. ; Codish, M. ; Gallagher, John Patrick ; Lagoon, V. / Combining norms to prove termination. Verification, model checking, and abstract interpretation, Third International Workshop, VMCAI 2002: Venice, Italy, January 21-22, 2002. red. / Agostino Cortesi. Springer, 2002. s. 126-138 (Lecture Notes in Computer Science, Bind 2294).
    @inbook{d29a5d7052bd11dba4bc000ea68e967b,
    title = "Combining norms to prove termination",
    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.",
    author = "S. Genaim and M. Codish and Gallagher, {John Patrick} and V. Lagoon",
    year = "2002",
    language = "English",
    isbn = "3-540-43631-6",
    pages = "126--138",
    editor = "Agostino Cortesi",
    booktitle = "Verification, model checking, and abstract interpretation, Third International Workshop, VMCAI 2002",
    publisher = "Springer",

    }

    Genaim, S, Codish, M, Gallagher, JP & Lagoon, V 2002, Combining norms to prove termination. i A Cortesi (red.), Verification, model checking, and abstract interpretation, Third International Workshop, VMCAI 2002: Venice, Italy, January 21-22, 2002. Springer, Lecture Notes in Computer Science, bind 2294, s. 126-138.

    Combining norms to prove termination. / Genaim, S.; Codish, M.; Gallagher, John Patrick; Lagoon, V.

    Verification, model checking, and abstract interpretation, Third International Workshop, VMCAI 2002: Venice, Italy, January 21-22, 2002. red. / Agostino Cortesi. Springer, 2002. s. 126-138 (Lecture Notes in Computer Science, Bind 2294).

    Publikation: Bidrag til bog/antologi/rapportBidrag til bog/antologiForskning

    TY - CHAP

    T1 - Combining norms to prove termination

    AU - Genaim, S.

    AU - Codish, M.

    AU - Gallagher, John Patrick

    AU - Lagoon, V.

    PY - 2002

    Y1 - 2002

    N2 - 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.

    AB - 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.

    M3 - Book chapter

    SN - 3-540-43631-6

    SP - 126

    EP - 138

    BT - Verification, model checking, and abstract interpretation, Third International Workshop, VMCAI 2002

    A2 - Cortesi, Agostino

    PB - Springer

    ER -

    Genaim S, Codish M, Gallagher JP, Lagoon V. Combining norms to prove termination. I Cortesi A, red., Verification, model checking, and abstract interpretation, Third International Workshop, VMCAI 2002: Venice, Italy, January 21-22, 2002. Springer. 2002. s. 126-138. (Lecture Notes in Computer Science, Bind 2294).