Proving Termination by Policy Iteration

In this paper, we explore the adaptation of policy iteration techniques to compute greatest fixpoint approximations, in order to find sufficient conditions for program termination. Restricting ourselves to affine programs and the abstract domain of template constraint matrices, we show that the abstract greatest fixpoint can be computed exactly using linear programming, and that strategies are related to the template constraint matrix used. We also present a first result on the relationships between this approach and methods which use ranking functions.