Termination Analysis of P-solvable Loops with Assignments Only

Automated termination analysis is important in the mechanic verification of many programs. However most of existed works analyze the termination based on the construction of linear ranking function. In this paper, we present an algorithm to analyze termination of P-solvable loops with assignments only. The algorithm is based on the recurrence solving and quantifier elimination. In order to prove termination, we check the condition which initial values should be satisfied. If the condition is false, then we can conclude the program is termination. Otherwise, we can give a counterexample to show the program is non-termination. The application of the algorithm is demonstrated on several examples.