@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",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "126--138",

editor = "Agostino Cortesi",

booktitle = "Verification, model checking, and abstract interpretation, Third International Workshop, VMCAI 2002",

}