良基归纳法在时序逻辑程序不变式验证中的应用

并发程序的不变式验证对理解程序和提高程序的正确性具有重要意义.以一种区间时序逻辑程序设计语言Framed Tempura为研究对象,给出了该语言的等价正则形,定义了该正则形在相邻两个状态上的良基关系,进而利用良基归纳法原理对该语言所描述的系统的不变式进行归纳验证.提出的基于良基归纳法的验证方法在时序逻辑程序中可以方便地验证系统的不变式,尤其是循环结构的不变量性质.     

基于QBF的循环不变式构造技术

构造循环不变式是程序验证的核心问题之一。主流的循环不变式构造方法通常假设程序中的变量在无限数域上取值,然而程序执行过程中变量都是用有限长度的位向量来表示,无限数域上的循环不变式在有限数域的程序中可能不再是不变式,反之亦然。针对这一问题,本文给出一种基于QBF求解的构造有限数域上循环不变式的方法。该方法可用于构造类型丰富的不变式,包括线性(或多项式)等式(或不等式)不变式,支持加、减、乘、除、移位、位操作等,允许不变式中出现量词。本文也例证了该方法在程序终止性证明、循环上界分析、程序正确性证明等方面的应用价值。     

基于遗传规划寻找循环不变式的方法

描述了一种产生循环不变式主要部分的方法。该方法的基本思想是在每一次循环条件变化时记录下程序变量的值,生成相应的跟踪表,从跟踪表中获得程序变量之间的函数关系构成循环不变式的主要部分。程序变量之间的函数关系则利用遗传规划对跟踪表中数据执行符号回归得到。     

利用基因表达式编程自动生成循环不变式

描述了利用基因表达式编程自动生成循环不变式的方法。该方法的基本思想是在每一次循环条件变化时记录下程序变量的值,产生相应的跟踪表,然后从跟踪表中获得程序变量之间的函数依赖关系,这种变量之间的依赖关系构成了循环不变式的主要部分。程序变量之间的函数依赖关系的获得是利用基因表达式编程对跟踪表中数据执行符号回归得到。利用VC＋＋实现了基因表达式编程的函数挖掘,并通过一个实例说明了该方法的有效性。     

一个面向C和Fortran数值程序的静态分析工具

程序的正确性验证一直以来都是计算机科学中的一个挑战性问题,抽象解释理论为程序静态分析提供了一个通用框架,可以在编译时自动地推导程序的动态性质。基于抽象解释的数值程序分析可以自动推导程序中数值变量间的不变式关系,这对于编译优化、程序错误检查至关重要。本文建立并实现了一个面向C和Fortran程序并支持过程间分析的数值程序分析框架和工具,C或Fortran源程序经过预处理后转化为具有统一格式的中间表示形式,然后基于该中间表示抽取与源程序语义等价的语义等式,最后在该语义等式上进行不动点迭代计算从而得到程序不变式。在此基础上,本文还对数组等复杂语法结构进行了建模和抽象。实验结果表明,该工具具有较高的可扩展性、精度,并能够处理大部分因数组的使用而带来的程序分析上的问题。     

CILinear:一个线性不变式自动构造工具

构造不变式是程序验证的重要组成部分,而开源工具Interpro。能对简单的程序设计语言构造线性不变式。基于Interproc和C程序编译工具CII,针对简化的C程序设计并实现了自动构造数值型程序变量线性不变式的工具CILinear,并与Interproc进行了比较。实验表明CILinear能有效地构造线性不变式,并且比Interproc支持的语法更多。通过实例讨论了CILinear在程序验证中的实际应用。     

一个基于Mathematica平台的程序安全性自动验证工具

程序安全性验证是程序验证的重要部分。基于不变式生成,将程序的安全性验证转化为验证不变式集合是否蕴含表示安全性的逻辑公式。针对简化的C程序,结合验证工具Theorema,在Mathematica平台上实现一个对程序安全性进行自动验证的工具。实验结果表明,该验证工具能够自动验证只含数值变量的C程序。     

基于算法框架的可重用部件设计与实现

对算法程序的功能规约进行等价变换,可以自然而且方便地得到求解问题设计思想的精确表达,即循环不变式。抽象算法又可以通过循环不变式获得。对算法程序中的算子进行提取、抽象就可以得到算法框架,而算法框架可以设计出可重用部件。文章通过对数组段极值问题的求解,展示了形式化推导不仅可以得到正确、高效的算法程序,而且具有软件重用的功能,并进一步给出了利用可重用部件求解数组段极值问题的C++实现。     

一种对象粒度的Java程序并发错误检测框架

由于多线程程序执行的复杂性和不确定性,Java程序中的并发错误难以被检测和修复.不变式检测方法作为目前最为有效的检测手段,采用提取正确程序行为的方式,能自动识别程序并发错误.但是,传统的不变式检测方法基于单个字段分析程序行为,不考虑程序中的关联变量间的依赖关系,所以无法检测多个关联变量引发的并发错误.针对这一问题,本文实现了一个对象粒度的不变式检测框架OBJ-D,基于对象操作分析程序行为.OBJ-D通过记录对象的读写依赖,能反映同一对象中多个变量间的依赖关系,为检测多变量并发错误创造了条件.测试表明,在不影响训练敏感度和性能开销的前提下,OBJ-D能同时有效检测单变量和多变量引发的并发错误,并只引入很少的假阳性.     

基于差分方程计算循环复杂度符号化上界

计算程序中循环的程序复杂度符号化上界可以验证程序的停机性.基于差分方程和最优化问题求解技术,给出了一种计算P*-solvable循环程序复杂度符号化上界的有效方法.分别针对含有赋值语句的循环和带条件分支的循环,提出了其程序复杂度符号化上界计算方法.与其他工作相比,该方法能够计算得到更精确的循环复杂度符号化上界,实验结果...     

Some Aspects of the Verification of Loop Computations

The problem of proving whether or not a loop computes a given function is investigated. We consider loops which have a certain "closure" property and derive necessary and sufficient conditions for such a loop to compute a given function. It is argued that closure is a fundamental concept in program proving. Extensions of the basic result to proofs involving relations other than functional relations, which typically arise in nondeterministic loops, are explored. Several applications of these results are given, particularly in showing that certain classes of programs may be directly proven (their loop invariants generated) given only their input-output relationships. Implications of these results are discussed.     

Proving termination of nonlinear command sequences

We describe a simple and efficient algorithm for proving the termination of a class of loops with nonlinear assignments to variables. The method is based on divergence testing for each variable in the cone-of-influence of the loop’s condition. The analysis allows us to automatically prove the termination of loops that cannot be handled using previous techniques. We also describe a method for integrating our nonlinear termination proving technique into a larger termination proving framework that depends on linear reasoning.     

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

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

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.     

Recent advances in program verification through computer algebra

In this paper, we summarize the results on program verification through semi-algebraic systems (SASs) 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.     

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

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

循环程序的界函数合成

作为循环程序终止性分析的主流方法,当前的秩函数方法大多局限于线性或多项式秩函数的求解。针对循环程序若不存在对应的线性或多项式秩函数,现有秩函数方法就无法证明其终止性的问题,提出一个新的方法来合成给定循环程序对应的界函数。对于给定的循环程序,倘若能找到其界函数,则表明该循环程序是可终止的。首先将界函数的求解问题转化为一个线性二分类问题,并在选定界函数模板后,根据模板建立映射关系以构建训练集;然后利用所得训练集通过支持向量机（SVM）获取分类超平面进而求解得到模板系数,从而得到候选的界函数;最后利用现有的符号验证工具Redlog对该候选界函数进行验证。实验结果表明,相较于现有的秩函数方法,所提方法不仅能够应用于更多的循环程序,而且所得界函数在形式上相较于秩函数更加简化。具体表现为,对于某些没有线性秩函数的循环,该方法可以得到其对应的线性界函数;同时,对于某些只有多阶段线性秩函数的循环,该方法可以求解得到全局的线性界函数。     

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.     

Invariant based programming: basic approach and teaching experiences

Program verification is usually done by adding specifications and invariants to the program and then proving that the verification conditions are all true. This makes program verification an alternative to or a complement to testing. We describe here another approach to program construction, which we refer to as invariant based programming, where we start by formulating the specifications and the internal loop invariants for the program, before we write the program code itself. The correctness of the code is then easy to check at the same time as one is constructing it. In this approach, program verification becomes a complement to coding rather than to testing. The purpose is to produce programs and software that are correct by construction. We present a new kind of diagrams, nested invariant diagrams, where program specifications and invariants (rather than the control) provide the main organizing structure. Nesting of invariants provide an extension hierarchy that allows us to express the invariants in a very compact manner. We have studied the feasibility of formulating specifications and loop invariants before the code itself has been written in a number of case studies. Our experience is that a systematic use of figures, in combination with a rough idea of the intended behavior of the algorithm, makes it rather straightforward to formulate the invariants needed for the program, to construct the code around these invariants and to check that the resulting program is indeed correct. We describe our experiences from using invariant based programming in practice, both from teaching programmers how to construct programs that they prove correct themselves, and from teaching invariant based programming for CS students in class. D. A. Duce, J. Oliveira, P. Boca and R. Boute