### Resumé

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

*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

}

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

Publikation: Bidrag til bog/antologi/rapport › Bidrag til bog/antologi › Forskning

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 -