Size-change termination and bound analysis
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
Size-change termination and bound analysis. / Avery, James Emil.
Functional and Logic Programming: 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006. Proceedings. ed. / Masami Hagiya; Philip Wadler. Springer, 2006. p. 192-207 (Lecture notes in computer science, Vol. 3945).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Size-change termination and bound analysis
AU - Avery, James Emil
N1 - Conference code: 8
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
KW - Faculty of Science
KW - automatisk programanalyse
KW - termineringsanalyse
KW - size-change grafer
KW - size-change termineringsanalyse
KW - konvekse polyeder
KW - konvekse hylstre
KW - abstrakt fortolkning
KW - automatic program analysis
KW - termination analysis
KW - size-change graphs
KW - size-change termination analysis
KW - convex polyhedra
KW - convex hulls
KW - abstract interpretation
U2 - 10.1007/11737414_14
DO - 10.1007/11737414_14
M3 - Article in proceedings
SN - 978-3-540-33438-5
T3 - Lecture notes in computer science
SP - 192
EP - 207
BT - Functional and Logic Programming
A2 - Hagiya, Masami
A2 - Wadler, Philip
PB - Springer
Y2 - 24 April 2006 through 26 April 2006
ER -
ID: 170215502