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

Originalsprog | Engelsk |
---|---|

Titel | Verification, model checking, and abstract interpretation, Third International Workshop, VMCAI 2002 : Venice, Italy, January 21-22, 2002 |

Redaktører | Agostino Cortesi |

Forlag | Springer |

Publikationsdato | 2002 |

Sider | 126-138 |

ISBN (Trykt) | 3-540-43631-6 |

Status | Udgivet - 2002 |

Navn | Lecture Notes in Computer Science |
---|---|

Vol/bind | 2294 |

ISSN | 0302-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