Size-Change Termination and Bound Analysis
Activity: Talk or presentation types › Lecture and oral contribution
James Emil Avery - Lecturer
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 (to be made 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.
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 (to be made 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.
16 Jul 2007
Event (Conference)
Title | Size-Change Termination and Bound Analysis |
---|---|
Date | 16/07/2007 → 16/07/2007 |
City | LIPN, Université Paris-Nord |
Country/Territory | France |
ID: 15433296