Title :
Termination of a Class of the Program with Polynomial Guards
Author :
Wu, Bin ; Shen, Liyong ; Bi, Zhongqin ; Zeng, Zhenbing
Author_Institution :
Shanghai Key Lab. of Trustworthy Comput., East China Normal Univ., Shanghai
Abstract :
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.
Keywords :
eigenvalues and eigenfunctions; polynomial matrices; program control structures; program verification; computer science; eigenvalue; linear assignment; loop program termination; matrix analysis; nonlinear polynomial guard; Bismuth; Buildings; Eigenvalues and eigenfunctions; Finite difference methods; Information management; Laboratories; Lagrangian functions; Piecewise linear techniques; Polynomials; Power engineering computing;
Conference_Titel :
Information Management and Engineering, 2009. ICIME '09. International Conference on
Conference_Location :
Kuala Lumpur
Print_ISBN :
978-0-7695-3595-1
DOI :
10.1109/ICIME.2009.102
