Regular approximation and bounded domains for size-change termination
Anderson, H. Khoo, S.-C.
Anderson, H.
Citations
Altmetric:
Alternative Title
Abstract
The size-change principle devised by Lee, Jones and Ben-Amram, provides an effective method of determining program termination for recursive functions. It relies on a regular approximation to the call structure of the program, operates only over variables whose "size" is well-founded, and ignores the conditionals and return values in the program. The main contribution of our paper is twofold: firstly we improve size-change termination analysis by using better regular approximations to program flow, and secondly we extend the analysis beyond the original well-founded variables to include integer variables. In addition, we pay attention to program conditionals that are expressed by linear constraints and support the analysis of functions in which the return values are relevant to termination. Our analysis is entirely mechanical, exploits the decidability and expressive power of affine constraints and extends the set of programs that are size-change terminating. Copyright © 2010 ACM.
Keywords
Affine size-change termination, Termination analysis
Source Title
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation
Publisher
Series/Report No.
Collections
Rights
Date
2010
DOI
10.1145/1706356.1706369
Type
Conference Paper