多项式循环程序的终止性研究及其应用

Analysis and verification of correctness of application-oriented software is of great significance. Termination analysis guarantees the complete correctness of software. For polynomial loop programs, this project will focus on the termination problem of the type of programs. By using symbolic-numeric computation tools, we will explore various verification techniques based on analysis of fixed points, invariant polytopes and Ranking functions. We will further study that the correlation between fix points and termination problems, and correlation between fix points and Ranking functions. Different from the existing methods of termination verification and analysis, the technique based on fixed points enables us not only to explore more loop programs whose termination can be proven to be decidable, but also to find Ranking functions over the integers. This work will make up for the deficiency of current termination analysis of polynomial programs. Moreover, this work is also very promising to be applied to verify and analyze the termination problems arising in embedded systems.

面向应用的软件正确性分析与验证具有十分重要的意义。终止性分析是保障程序完全正确性的必要基础。嵌入式软件中的循环程序往往具有多项式结构。因此，本课题针对多项式循环程序的非线性性、动力行为的不确定性等特点，围绕多项式循环程序的终止性验证这一大难题，采用符号数值混合计算理论及工具，深入探索基于不动点技术、 多面体不变集分析以及秩函数计算的终止性验证理论和算法。其中，着重研究不动点理论与终止性问题的内在联系以及与秩函数之间的深刻关系。不同于现有终止性验证方法，我们提出的基于不动点分析的验证技术不仅能在终止性这一不可判定问题中探测到更多的终止性可判定子类，而且能将秩函数合成问题从实域上拓展到整数环上，为终止性问题的研究提供了新的研究手段和方法，丰富了终止性验证的基础理论。这项研究将弥补目前在非线性多项式循环程序终止性验证方面研究的不足。同时，研究结果有望广泛应用于嵌入式软件的终止性分析与验证中。

本项目运用计算机代数的理论和工具，围绕程序终止性这一问题，从可判定性，秩函数构造与计算等方面，对多项式循环程序的终止性问题进行了研究。对线性循环程序，我们首次证明了这类循环不可终止的充分必要条件是循环条件形成的区域中存在多面体吸引集，并给出了该吸引集的代数刻画。与传统方法不同，新的方法并不依赖Jordan标准型的计算，从而避免了Jordan标准型的浮点计算所造成的判定误差。该成果发表在国际期刊Theoretical Computer Science. 非线性循环程序由于更为复杂的动力行为，使得当前从可判定角度对其研究的结果甚少。基于函数不动点理论，我们建立了适定条件，使得在该条件下，可将这类循环程序的终止性问题等价地归结为不动点的判定，为非线性循环程序的终止性研究提供了新的研究手段和方法。相关成果发表在ICTAC 2016，SETTA 2017，软件学报等会议期刊上。秩函数（Ranking Functions）法仍是当前终止性研究的主流方法。从几何角度，我们对线性秩函数的构造做了深入分析，建立了线性程序不存在线性秩函数的witness points的代数刻画。不同于现有方法，我们的方法揭示了线性秩函数与状态点集间的内在关联。该成果发表在国际期刊STTT上。但程序的秩函数未必是线性的。针对非线性多项式型秩函数的计算问题，我们提出两种途径来解决它。一是利用Polya定理，将多项式秩函数计算问题归结为线性约束求解问题，从而便于利用线性规划算法进行求解。实验表明该方法效率上优于传统的量词消去方法。二是我们证明了秩函数计算问题等价于在两个点集间超平面的计算问题，继而利用机器学习算法探寻候选秩函数，并借助符号计算工具对其予以精确验证。上述系列成果已发表在软件学报，ICFEM 2019，STTT上。此外，我们提出了L-eventual 秩函数及局部秩函数的概念。实验表明，对于部分没有传统秩函数的程序，我们发现它们的确具有L-eventual秩函数或局部秩函数。相关成果已发表在TASE 2016，ESTC 2018上。本项目中，基于不动点分析的工作丰富了当前终止性研究的基础理论，为我们今后在终止性方面的研究提供了可持续的科研思路。