Combining Norms to Prove Termination

S Genaim, M Codish, J Gallagher, V Lagoon

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

19 Citations (Scopus)


Automatic termination analysers typically measure the size of terms applying norms which are mappings from terms to the natural numbers. This paper illustrates how to 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.
Translated title of the contributionCombining Norms to Prove Termination
Original languageEnglish
Title of host publicationUnknown
EditorsA. Cortesi
PublisherSpringer Berlin Heidelberg
Pages126 - 138
Number of pages12
ISBN (Print)3540436316
Publication statusPublished - Apr 2002

Bibliographical note

Conference Proceedings/Title of Journal: Verification, Model Checking, and Abstract Interpretation, Third International Workshop, VMCAI 2002.


Dive into the research topics of 'Combining Norms to Prove Termination'. Together they form a unique fingerprint.

Cite this