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

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

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

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

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

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

循环程序的界函数合成

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

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

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

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

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

基于Dixon结式和逐次差分代换的多项式秩函数探测方法

秩函数探测是循环程序终止性分析的重要方法，目前，已有很多研究者致力于为线性循环程序探测对应的线性秩函数，然而，针对具有多项式循环条件和多项式赋值的多项式型的循环，现有的秩函数探测方法还有所不足，解决方案大多是不完备的、或者具有较高的时间复杂度。针对现有工作对于多项式秩函数探测方法不足的问题，基于扩展Dixon结式（KSY方法）和逐次差分代换（SDS）方法，提出一种为多项式循环程序探测多项式型秩函数的方法。首先，将待探测的秩函数模板看作带参数系数的多项式，将秩函数的探测转换为寻找满足条件的参数系数的问题；然后，进一步将问题转换为判定相应的方程组是否有解的问题，至此，利用KSY方法中的扩展的Dixon结式，将问题更进一步简化为带参系数多项式（即结式）严格为正的判定问题；最后，利用SDS方法，找到一个充分条件，使得得到的结式严格为正，此时，可以获取满足条件的参数系数的取值，从而找到一个满足条件的秩函数，通过实验验证该秩函数探测方法的有效性。实验结果表明，利用该方法，可以有效地为多项式循环程序找到多项式秩函数，包括深度为d的多阶段多项式秩函数，与已有方法相比，该方法能够更高效地找到多项式秩函数，对于基于柱形代数分解（CAD）方法的探测方法因时间复杂度问题无法而应对的一些循环，利用所提方法能够在几秒内为这些循环找到秩函数。     

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

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

有界闭区间并上的非线性循环程序的终止性验证

利用符号动力学理论中有关一维离散映射的函数和区间的转换图方法及相关结论,证明一类非线性循环程序不终止的必要条件是在该程序循环区间上有不动点或者周期点存在,并给出相应的终止性验证算法.利用该算法可以验证一维有界闭区间上的非线性循环程序的终止性.最后,给出计算实例演示该算法的算法步骤.     

基于基因表达式编程的错误定位方法

错误定位是软件调试中最重要且最耗时的部分,错误定位中的任何改进都可以大大降低软件成本,而其中秩函数的选择问题则尤为关键。结合基因表达式编程技术以及基于频谱的错误定位算法,找到适应程序的高效秩函数,提出了一种新的错误定位方法。从程序测试用例的覆盖信息中提取出四种类型的子集信息;通过基因表达式编程训练出适应程序的最优秩函数;利用秩函数计算出每条语句的可疑度值,并按照可疑度值由高到低的顺序逐条检查程序的可疑语句进行错误定位。通过实验,将训练出的秩函数与已经提出的秩函数（如Tarantula,Ochiai等）进行比较分析,结果表明,基于基因表达式编程的错误定位方法具有更精确的错误定位效果和更显著的定位效率。     

Quantum loop programs

Loop is a powerful program construct in classical computation, but its power is still not exploited fully in quantum computation. The exploitation of such power definitely requires a deep understanding of the mechanism of quantum loop programs. In this paper, we introduce a general scheme of quantum loops and describe its computational process. The function computed by a quantum loop is defined, and a denotational semantics and a weakest precondition semantics of a quantum loop are given. The notions of termination and almost termination are proposed for quantum loops. This paper only consider the case of finite-dimensional state spaces. Necessary and sufficient conditions for termination and almost termination of a general quantum loop on any mixed input state are presented. A quantum loop is said to be (almost) terminating if it (almost) terminates on any input state. We show that a quantum loop is almost terminating if and only if it is uniformly almost terminating. It is observed that a small disturbance either on the unitary transformation in the loop body or on the measurement in the loop guard can make any quantum loop (almost) terminating, provided that some dimension restriction is satisfied. Moreover, a representation of the function computed by a quantum loop is given in terms of finite summations of matrices. To illustrate the notions and results obtained in this paper, two simple classes of quantum loop programs, one qubit quantum loops, and two qubit quantum loops defined by controlled gates, are carefully examined, and to show their expressive power, quantum loops are applied in describing quantum walks.     

Recent advances in program verification through computer algebra

In this paper, we summarize the results on program verification through semi-algebraic systemsSASs solving that we have obtained, including automatic discovery of invariants and ranking functions, symbolic decision procedure for the termination of a class of linear loops, termination analysis of nonlinear systems, and so on.     

Fair termination revisited—with delay

A proof method for establishing the fair termination and total correctness of both nondeterministic and concurrent programs is presented. The method calls for the extension of state by auxiliary delay variables which count down to the instant in which certain action will be scheduled. It then uses well-founded ranking to prove fair termination allowing nested fair selection and loops.     

Manifold Ranking using Hessian Energy

In recent years, learning on manifolds has attracted much attention in the academia community. The idea that the distribution of real-life data forms a low dimensional manifold embedded in the ambient space works quite well in practice, with applications such as ranking, dimensionality reduction, semi-supervised learning and clustering. This paper focuses on ranking on manifolds. Traditional manifold ranking methods try to learn a ranking function that varies smoothly along the data manifold by using a Laplacian regularizer. However, the Laplacian regularization suffers from the issue that the solution is biased towards constant functions. In this work, we propose using second-order Hessian energy as regularization for manifold ranking. Hessian energy overcomes the above issue by only penalizing accelerated variation of the ranking function along the geodesics of the data manifold. We also develop a manifold ranking framework for general graphs/hypergraphs for which we do not have an original feature space (i.e. the ambient space). We evaluate our ranking method on the COREL image dataset and a rich media dataset crawled from Last.fm. The experimental results indicate that our manifold ranking method is effective and outperforms traditional graph Laplacian based ranking method.