Termination of a Class of the Program with Polynomial Guards
Bin Wu, Li‐Yong Shen, Zhongqin Bi, Zhenbing Zeng · 2009
Determining the termination of programs is a basic task in computing science. By analyzing the powers of a matrix symbolically using its eigenvalues, this paper presents a method to prove termination of a class of loop programs with nonlinear guards and linear assignments. The termination of a linear assignment loop is only decided by the eigen values, whose module is greater than one, of the matrix defining the loop assignments.