Size-change termination and bound analysis

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Despite its simplicity, the size-change termination principle, presented by Lee, Jones and Ben-Amram in [LJB01], is surprisingly strong and is able to show termination for a large class of programs. A significant limitation for its use, however, is the fact that the SCT requires data types to be well-founded, and that all mechanisms used to determine termination must involve decreases in these global, well-founded partial orders. Following is an extension of the size-change principle that allows for non-well founded data types, and a realization of this principle for integer data types. The extended size-change principle is realized through combining abstract interpretation over the domain of convex polyhedra with the use of size-change graphs. In the cases when data types are well founded, the method handles every case that is handled by LJB size-change termination. The method has been implemented in a subject language independent shared library, libesct (available at http://esct.kvante.org), as well as for the ANSI C specializer C-Mix/ii, handling a subset of its internal language Core-C.
Original languageEnglish
Title of host publicationFunctional and Logic Programming : 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006. Proceedings
EditorsMasami Hagiya, Philip Wadler
Number of pages16
PublisherSpringer
Publication date2006
Pages192-207
ISBN (Print)978-3-540-33438-5
ISBN (Electronic)978-3-540-33439-2
DOIs
Publication statusPublished - 2006
Event8th International Symposium on Functional and Logic Programming - Fuji-Susono, Japan
Duration: 24 Apr 200626 Apr 2006
Conference number: 8

Conference

Conference8th International Symposium on Functional and Logic Programming
Nummer8
LandJapan
ByFuji-Susono
Periode24/04/200626/04/2006
SeriesLecture notes in computer science
Volume3945
ISSN0302-9743

    Research areas

  • The Faculty of Science - automatic program analysis, termination analysis, size-change graphs, size-change termination analysis, convex polyhedra, convex hulls, abstract interpretation

ID: 170215502