多项式循环程序的秩函数探测

秩函数法是循环程序终止性分析的主流方法.针对一类多分支多项式循环程序,这类程序的秩函数计算问题被证明可归结为单形上正定多项式的探测问题,从而便于利用线性规划工具Simplex去计算这类程序的秩函数.不同于现有基于柱形代数分解的量词消去算法,该方法能够在可接受的时间内计算更为复杂的多项式秩函数.     

基于SVM的多项式循环程序秩函数生成

程序终止性问题是自动程序验证领域中的一个研究热点.秩函数探测是进行终止性分析的主要方法.针对单重无条件分支的多项式循环程序,将其秩函数计算问题归结为二分类问题,从而可利用支持向量机（SVM）算法来计算程序的秩函数.与基于量词消去技术的秩函数计算方法不同,该方法能在可接受的时间范围内探测到更为复杂的秩函数.     

循环程序的界函数合成

作为循环程序终止性分析的主流方法,当前的秩函数方法大多局限于线性或多项式秩函数的求解.针对循环程序若不存在对应的线性或多项式秩函数,现有秩函数方法就无法证明其终止性的问题,提出一个新的方法来合成给定循环程序对应的界函数.对于给定的循环程序,倘若能找到其界函数,则表明该循环程序是可终止的.首先将界函数的求解问题转化为一个...     

单分支线性约束循环程序的终止性分析

秩函数法是循环终止性分析的主要方法,秩函数的存在表明了循环程序是可终止的.针对单分支线性约束循环程序,提出一种方法对此类循环的终止性进行分析.基于增函数法向空间的计算,该方法将原程序空间上的秩函数计算问题归结为其子空间上的秩函数计算问题.实验结果表明,该方法能有效验证现有文献中大部分循环程序的终止性.     

基于深度学习和反例制导的循环程序秩函数生成

程序终止性判定是程序分析与验证领域中的一个研究热点. 针对非线性循环程序, 提出了一种基于反例制导的神经网络型秩函数的构造方法. 该方法采用学习组件和验证组件交互的迭代框架, 其中学习组件利用程序轨迹作为训练集合构造一个候选秩函数, 验证组件运用可满足性模理论(Satisfiability Modulo Theories, SMT)确保候选秩函数的有效性, 而由SMT返回的反例则进一步用于扩展学习组件中的训练集合以对候选秩函数进行精化.实验结果表明, 所提出的方法比已有的机器学习方法在秩函数的构造效率和构造能力上具有优势.     

基于k阶秩函数的线性赋值循环程序的终止性分析

循环程序的终止性是确保循环程序完全正确的必要条件。 如果给定的线性赋值循环程序不存在传统定义的线性秩函数,那么基于传统定义的秩函数终止性证明方法将失效。基于Aⁿx的精确计算,对传统的秩函数概念进行了扩展,提出了k阶秩函数的概念。使用RegularChains软件包给出了合成k阶秩函数的具体方法。实验结果表明,相比于传统定义的线性秩函数,k阶秩函数的适应范围更广。对于 不能用传统定义的秩函数证明其终止性的部分循环程序,可以基于k阶秩函数来证明,从而体现了所提方法的优越性。     

基于迭代轨迹划分的单分支循环程序终止性分析

秩函数作为循环程序终止性分析的重要方法已得到广泛研究。文中着重研究了单分支循环的终止性。首先提出了双向迭代循环概念，将单分支循环分为双向迭代循环和非双向迭代循环。其次，针对双向迭代循环程序，建立了一种划分思路，提出了三段式秩函数的概念，并证明了若该双向迭代循环存在三段式秩函数，则其是终止的。而对非双向迭代循环，引用增函数的划分思路，即利用增函数将原程序空间划分为更小的空间，并通过计算更小空间上的秩函数来证明原程序的终止性。最后，将三段式秩函数的计算问题归结为SVM分类问题，并利用工具Z3或bottema对由SVM所得的候选秩函数进行验证。     

Dixon结式在密码学中的应用

针对密码学中的多变元多项式二次方程系统求解问题,基于扩展Dixon结式提出了一种求解算法DR(Dixon resultants).基本思想为对于MQ(multivariate quadratic)问题,把x₁,x₂,…,x_n-1当作变元,而把x_n当作参数,然后利用和改进扩展Dixon结式方法求解该类系统.分析了该算法对于一般情况的复杂度,并且基于实验证据猜测:对于某些稀疏问题,新算法的复杂度很有可能也是多项式的.实验结果表明,对于m=n的一般和稀疏的问题,DR效率优于已有的两种算法.除了高效性,新算法还具有复杂度容易度量、计算时间可以预测的优点.     

计算最终线性秩函数的新方法

程序的终止性分析作为程序验证中重要的一环,在软件正确性验证中极为重要。对于一个线性循环程序,若该程序没有传统定义的线性秩函数,则基于传统定义的秩函数终止性分析方法失效。2013年,Bagnara提出了最终线性秩函数(Eventual Linear Ranking Functions)的定义,并证明了若某个程序存在最终线性秩函数,则该程序终止。由此,提出了新的方法来计算最终线性秩函数,构造了存在线性增函数和最终线性秩函数的等价半代数系统,并使用Mathematica工具对半代数系统进行求解,对比分析了各种最终秩函数求解方法的实际计算时间,结果证实了所提方法的优越性。     

多项式族稳定性判定问题的多项式算法

利用除零原则,多项式族稳定性的判定问题(系数仿射依赖于参数的情形)可以化为单参 数秩2简单二次规划问题.本文用二次规划的理论、Kuhn-Tucker条件,提出了此问题的一 个多项式时间算法.可以看到许多重要的结果,如棱边定理和强Kharitonov定理仅是此算 法的一个特例.作为简单应用,介绍了区间多项式族Schur问题的一个具体算例.     

Cayley–Dixon projection operator for multi-univariate composed polynomials

The Cayley–Dixon formulation for multivariate projection operators (multiples of resultants of multivariate polynomials) has been shown to be efficient (both experimentally and theoretically) for simultaneously eliminating many variables from a polynomial system. In this paper, the behavior of the Cayley–Dixon projection operator and the structure of Dixon matrices are analyzed for composed polynomial systems constructed from a multivariate system in which each variable is substituted by a univariate polynomial in a distinct variable. Under some conditions, it is shown that a Dixon projection operator of the composed system can be expressed as a power of the resultant of the outer polynomial system multiplied by powers of the leading coefficients of the univariate polynomials substituted for variables in the outer system. A new resultant formula is derived for systems where it is known that the Cayley–Dixon construction does not contain any extraneous factor. The complexity of constructing Dixon matrices and roots at toric infinity of composed polynomials is analyzed.     

Termination of linear programs with nonlinear constraints

Tiwari (2004) proved that the termination problem of a class of linear programs (loops with linear loop conditions and updates) over the reals is decidable through Jordan forms and eigenvector computation. Braverman (2006) proved that it is also decidable over the integers. Following their work, we consider the termination problems of three more general classes of programs which are loops with linear updates and three kinds of polynomial loop conditions, i.e., strict constraints, non-strict constraints and both strict and non-strict constraints, respectively. First, we prove that the termination problems of such loops over the integers are all undecidable. Then, for each class we provide an algorithm to decide the termination of such programs over the reals. The algorithms are complete for those programs satisfying a property, Non-Zero Minimum.     

多分支单变量循环程序的终止性分析

对多分支单变量循环程序的终止性问题进行了研究.证明了在适定的条件下,该类循环程序不可终止性的充分必要条件是迭代映射在循环条件形成的区域中有不动点.特别地,当这类循环程序是多项式循环程序时,在给定条件下,其在实数域上的终止性问题是可判定的.     

Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods

We present a symbolic-numeric hybrid method, based on sum-of-squares (SOS) relaxation and rational vector recovery, to compute inequality invariants and ranking functions for proving total correctness and generating preconditions for programs. The SOS relaxation method is used to compute approximate invariants and approximate ranking functions with floating point coefficients. Then Gauss-Newton refinement and rational vector recovery are applied to approximate polynomials to obtain candidate polynomials with rational coefficients, which exactly satisfy the conditions of invariants and ranking functions. In the end, several examples are given to show the effectiveness of our method.     

常用循环摘要的自动生成方法及其应用

采用形式化方法证明软件的正确性是保障软件可靠性的有效方法,而对循环语句的分析与验证是形式化证明中的关键,对循环语句的处理一直是程序分析与验证中的一个难点问题.本文提出使用循环语句修改的内存和这些内存中存放的新值来描述循环语句的执行效果,并将该执行效果定义为循环摘要.同时,本文提出了一种自动生成循环摘要的方法,可以为操作常用数据结构的循环自动生成循环摘要,包含嵌套循环.此外,基于循环摘要,我们可以自动生成循环语句的规约,包括循环不变式、循环的前置条件以及循环的后置条件.我们已经实现了自动生成循环摘要以及循环规约的方法,并将它们集成到验证工具Accumulator中,实验表明,我们的方法可以有效地生成循环摘要,并生成多种类型的规约,从而辅助软件程序的形式化证明,提高验证的自动化程度和效率,减轻验证人员的负担.