Termination analysis of loop programs is very important in many applications, especially in those of safety critical software. In this paper, the termination of programs with polynomial guards and linear assignments is simplified to decide solvability of semi-algebraic systems(SAS). If the number of functions are finite or the functions are integer periodic, then the termination of programs is decidable. The discussion is based on simplifying the linear loops by its Jordan form. And then the process to find the nonterminating points for general polynomial guards is proposed. For avoiding floating point computations in the process, a symbolic algorithm is given to compute the Jordan form of a matrix. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Wu, B., Shen, L., Bi, Z., & Zeng, Z. (2010). Termination of loop programs with polynomial guards. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6019 LNCS, pp. 482–496). Springer Verlag. https://doi.org/10.1007/978-3-642-12189-0_42
Mendeley helps you to discover research relevant for your work.