Termination analysis with recursive calling graphs

Termination analysis has been studied for many years. The size-change termination principle proposed by Lee, Jones and Ben-Amram in 2001 is an effective method for automatic termination analysis. The principle ignores the condition and return values for function call. In this paper, we devise a new method for termination analysis over the integer domain by reconsidering the ignoring features. The main contribution of our paper with recursive calling graphs is twofold: firstly, it supports the analysis of functions in which the return values are relevant to termination. Secondly, it gains more accuracy for oscillating value change in termination analysis.