基于不变式生成的循环停机性验证

循环的停机性验证是程序验证中的一个难点。程序不变式用来描述程序变量的取值关系,其中线性不变式可以帮助描述程序变量间的线性关系,循环不变式能够有效刻画循环中的变量关系。本文基于线性不变式和多项式循环不变式的生成,将循环的停机性验证转化为求解一个最优化问题,给出了一个实用的程序停机性验证框架。基于该框架可以自动地验证程序的停机性,并给出循环的复杂度上界。实验结果说明了该方法的实用性。     

基于DISCOVERER的Petri网不变式自动生成*

在Petri网的验证中,代数不变式起着非常重要的作用。将Petri网建模为半代数变迁系统,提出了自动生成不变式的算法,该不变式有助于更好地分析Petri网可达空间。算法首先将Petri网的不变式假定为一个含参数系统,然后通过求解半代数系统来求解不变式中的参数;最后,基于DISCOVERER和QEPCAD等Maple软件包实现了该算法,并通过实例说明了算法的有效性。     

区间非线性路径约束的动态优化问题求解

本文研究路径约束中含有区间参数形式的动态优化问题,提出了一种新的非线性路径约束的确定化描述形式,和采用惩罚函数法的求解算法。对于转化后的极大极小优化命题,论文提出采用Lagrangian多项式加权和的方法得到有限维的确定性优化求解形式。该算法可有效地描述和求解不确定参数动态优化问题。     

一种形式化开发非递归算法的方法*

提出了一种简单、统一的形式化开发非递归算法的方法.该方法直接面向非递归算法,在形式化方法PAR的指导下,使用循环不变式的开发新策略,在得到求解递归问题的循环不变式的同时,能直接得到易读、高效且可靠的非递归算法,并通过一个具体实例进行了阐述.对使用形式化方法及循环不变式开发新策略开发非递归算法的方法作了较深入的实践和探讨.     

循环不变式开发技术研究

高可靠性软件是当今软件开发的热点问题。确保算法程序逻辑结构正确最理想的途径是算法程序的形式化推导和证明,而循环不变式是算法程序形式推导和证明的关键。循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也是最困难的问题之一。本文研究了众多现有循环不变式开发方法中较为典型的几种方法,指出了它们的基本原理、技术难点、特点及效果,旨在探寻循环不变式本质特征,从而为研究更简单、有效的生成方法提出指导。     

命令式动态规划类算法程序推导及机械化验证

动态规划是一种递归求解问题最优解的方法,主要通过求解子问题的解并组合这些解来求解原问题.由于其子问题之间存在大量依赖关系和约束条件,所以验证过程繁琐,尤其对命令式动态规划类算法程序正确性验证是一个难点.基于动态规划类算法Isabelle/HOL函数式建模与验证,通过证明命令式动态规划类算法程序与其的等价性,避免证明正确性时处理复杂的依赖关系和约束条件,提出命令式动态规划类算法程序设计框架及其机械化验证.首先,根据动态规划类算法的优化方法(备忘录方法)和性质(最优子结构性质和子问题重叠性质)描述问题规约、归纳递推关系式和形式化构造出循环不变式,并且基于递推关系式生成IMP (Minimalistic Imperative Programming Language)代码;其次,将问题规约、循环不变式和生成的IMP代码输入VCG (Verification Condition Generator),自动生成正确性的验证条件;然后,在Isabelle/HOL定理证明器中对验证条件进行机械化验证.算法首先设计为命令式动态规划类算法的一般形式,并进一步实例化得到具体算法.最后,例证了所提框架的有效性,为动态规划类算法的自动化推导和验证提供参考价值.     

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

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

求解含非线性参数的QoS路由的启发式算法

具有非线性参数的QoS路由分为含有非线性约束条件的QoS路由和含有非线性优化目标的QoS路由两类，它们都是NP问题．提出了两种启发式算法求解这两类QOS路由优化问题问题．对第一类问题，求解去掉非线性约束条件后的优化问题．如果找到的解满足非线性约束条件，则该解是最优解；否则在优化问题中添加一个新的线性约束，将已得到的解去掉，反复下去就可得到最终解．对第二类问题，将非线性优化目标换为约束条件中的线性参数，求解此优化模型，如果有解，则记录此时对应的非线性目标值．而后增加一个新的线性约束，去掉刚才得到的解，比较两次得到的非线性目标值，保留最小值．如果得到的解不满足该线性参数的约束条件，则算法结束；否则继续迭代．证明了两种算法的收敛性，并且时间复杂性为近似多项式时间．计算实例表明了算法的有效性．     

形式化开发Hanoi塔问题非递归算法

使用形式化方法PAR及循环不变式开发新策略,开发了Hanoi塔问题非递归算法,并对其进行了形式化地正确性证明。本文直接面向非递归算法,在得到求解Hanoi塔问题的循环不变式的同时,直接得到易读、高效且可靠的非递归算法。对使用形式化方法及循环不变式开发新策略开发非递归算法作了较深入的实践和探讨。     

后序遍历二叉树非递归算法的推导及形式化证明

开发涉及非线性数据结构算法程序的循环不变式一直是形式化方法的难点。本文使用PAR方法开发循环不变式的新策略,对后序遍历二叉树问题循环不变式的开发使用递归定义技术,得到了该问题循环不变式的简单精确的表达形式,简化了算法程序的推导和证明过程;利用PAR平台提供的抽象程序设计语言Ap1a中的数据抽象机制,使所得的算法程序结构简洁清晰且易于证明;最后,使用Dijkstra-Gries标准程序证明法形式证明了该问题的核心算法程序(只有4行代码),并使用PAR平台将Apla程序转换成正确的C++代码。实例的成功进一步说明PAR方法提供的循环不变式的开发技术对推导和证明非线性数据结构算法程序的有效性。     

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

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

循环不变式开发新策略及其应用

循环不变式体现了循环程序的本质特征,在算法程序的开发、证明和推导中具有十分重要的作用。而传统的循环不变式开发策略并没有很好地解决循环不变式开发难的问题。文章在阐述现有策略局限性的基础上,详细阐述了刻画循环不变式本质特征的新定义及基于此定义的开发循环不变式的新策略,并通过三个典型的实例,对开发新策略的具体应用作了比较深入的探索。     

A self-organized model for the control,planning and learning of nonlinear multi-dimensional systems using a sensory feedback

A new approach is presented to deal with the problem of modelling and simulating the control mechanisms underlying planned-arm-movements. We adopt a synergetic view in which we assume that the movement patterns are not explicitly programmed but rather are emergent properties of a dynamic system constrained by physical laws in space and time. The model automatically translates a high-level command specification into a complete movement trajectory. This is an inverse problem, since the dynamic variables controlling the current state of the system have to be calculated from movement outcomes such as the position of the arm endpoint. The proposed method is based on an optimization strategy: the dynamic system evolves towards a stable equilibrium position according to the minimization of a potential function. This system, which could well be described as a feedback control loop, obeys a set of non-linear differential equations. The gradient descent provides a solution to the problem which proves to be both numerically stable and computationally efficient. Moreover, the addition into the control loop of elements whose structure and parameters have a pertinent biological meaning allows for the synthesis of gestural signals whose global patterns keep the main invariants of human gestures. The model can be exploited to handle more complex gestures involving planning strategies of movement. Finally, the extension of the approach to the learning and control of non-linear biological systems is discussed.     

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     

含有析取语义循环的不变式生成改进方法

抽象解释为程序不变式的自动化生成提供了通用的框架,但是该框架下的大多数已有数值抽象域只能表达几何上是凸的约束集.因此,对于包含(所对应的约束集是非凸的)析取语义的特殊程序结构,采用传统数值抽象域会导致分析结果不精确.针对显式和隐式含有析取语义的循环结构,提出了基于循环分解和归纳推理的不变式生成改进方法,缓解了抽象解释分析中出现的语义损失问题.实验结果表明:相比已有方法,该方法能为这种包含析取语义的循环结构生成更加精确的不变式,并且有益于一些安全性质的推理.     

Predicate abstraction in a program logic calculus

Predicate abstraction is a form of abstract interpretation where the abstract domain is constructed from a finite set of predicates over the variables of the program. This paper explores a way to integrate predicate abstraction into a calculus for deductive program verification based on symbolic execution, where it allows us to infer loop invariants automatically that would otherwise have to be given interactively. The approach has been implemented as a part of the KeY verification system.     

Class invariants as abstract interpretation of trace semantics

We present a generic framework for the automatic and modular inference of sound class invariants for class-based object-oriented languages. We define a trace-based semantics for classes which considers all possible orderings, with all possible arguments, of invocations of all the methods of a class. We prove a correspondence theorem between such a semantics and a generic, trace-based, semantics for complete object-oriented programs.We express state-based class invariants in a fixpoint form by considering an abstraction of the class semantics, and we show how class invariants can be automatically inferred exploiting a static analysis of the methods. Furthermore, we address the problem of inferring a subclass invariant without accessing to the parent code, but just to its invariant.