Termination Analysis of linear Loop Programs

摘要

We observe that the termination of linear programs relies only on the initial value of program variables and the iteration count. Based on such observation, we present a constructive approach to determine the termination of linear programs. Through our approach, we can also synthesis the termination condition of linear programs if they do not terminate on all inputs, and correct termination defect.