Termination of Loop Programs with Polynomial Guards
Termination of Loop Programs with Polynomial Guards
复制标题
DOI：
10.1007/978-3-642-12189-0_42
复制
发表时间：
2010-03
期刊：
影响因子：
--
通讯作者：
Bin Wu;L. Shen;Zhongqin Bi;Zhenbing Zeng
中科院分区：
文献类型：
--
作者：
Bin Wu;L. Shen;Zhongqin Bi;Zhenbing Zeng
循环程序的可终止性分析在许多应用中非常重要，特别是在安全关键软件中。本文将多项式保护和线性配置程序的终止性简化为判定半代数系统（SAS）的可解性。如果函数的个数是有限的或函数是整数周期的，则程序的终止是可判定的。讨论的基础上简化的线性回路的约旦形式。在此基础上，给出了一般多项式保护的非终止点的求解过程。为了避免计算过程中的浮点运算，给出了计算矩阵Jordan形的符号算法。
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.