《程序验证关键技术研究》由会员分享，可在线阅读，更多相关《程序验证关键技术研究（108页珍藏版）》请在金锄头文库上搜索。
1、国防科学技术大学 博士学位论文 程序验证关键技术研究 姓名：邢建英 申请学位级别：博士 专业：计算机科学与技术 指导教师：李舟军 2011-03 国防科学技术大学研究生院博士学位论文 第 i 页 摘 要 程序验证是保证程序正确性的关键技术。停机性和安全性验证是程序验证中 的两个重要研究内容，受到了大量关注和广泛研究。 本文针对程序的停机性和安全性验证进行了系统、深入的研究，主要工作包 括以下几个方面： 1. 基于最优化问题提出了一种线性秩函数构造技术。首先设置线性秩函数模 板和模板中参数的取值区间，并在取值区间内对线性秩函数模板中的参数进行实 例化，然后以循环不变式作为最优化问题的约束系统，以
2、实例化的线性秩函数模 板的差分作为最优化问题的目标，构造最优化问题并进行求解。最优化问题的最 优解给出了线性秩函数递减的最小步长，因而可以进一步应用于计算循环精确的 符号化复杂度上界。基于最优化问题的秩函数构造方法不但能够验证线性程序和 多项式程序的停机性，而且可以验证某些含有指数或对数函数的非多项式程序的 停机性。 2. 基于不变式生成技术提出了验证程序停机性和安全性的框架。将程序不变 式视为程序变量的约束系统。通过引入不变式集，给出了验证程序停机性和安全 性的新方法。通过插桩循环计数器将循环停机性的验证转化为求解一个最优化问 题，其中最优化问题的约束系统为循环出口的所有程序不变式集合，最优
3、化问题 的目标函数是计算循环计数器的最小值。 使用这种方法， 将不再需要求解秩函数， 并且对某些不存在秩函数的循环也可以验证其停机性。本文还提出了基于定理证 明器验证逻辑蕴涵关系的安全性验证方法，将安全性的验证转化为验证不变式集 合是否蕴含由描述安全性的逻辑公式。由于在每个程序点都可以生成不变式集合， 不需要采用计算最弱前置条件，降低了自动验证的难度。 3. 基于差分方程和最优化问题，提出了一种循环符号化复杂度上界的计算方 法。循环符号化复杂度上界是循环执行次数的一个符号化上界，它可以衡量程序 的时间复杂度，也可以用于验证程序的停机性。首先用差分方程刻画循环中变量 取值的变化，并求解出差分方程
4、的闭合形式解。然后以差分方程的闭合形式解和 循环条件取反作为最优化问题的约束系统，以表示循环执行次数的变量作为最优 化问题的目标，构造最优化问题并进行求解。最优化问题的解就是循环符号化复 杂度上界。这种方法可以验证不存在秩函数并且不存在多项式等式循环不变式的 程序的停机性，与其他工作比较，基于差分方程和最优化问题能够给出更精确的 符号化复杂度上界。 4. 条件停机验证的目的是构造程序停机的前置条件。基于 polyranking 方法和 约束求解，提出了一种条件停机验证方法，对于具有阶段变化（phase- change）的 国防科学技术大学研究生院博士学位论文 第 ii 页 程序，能够直接计算出
5、所期望的停机前置条件，与其他方法相比，具有更好的计 算效率。 关键词：程序验证；停机性；秩函数；最优化问题；不变式；安全性；复杂 度上界；条件停机 国防科学技术大学研究生院博士学位论文 第 iii 页 Abstract Program verification is the key method for ensuring correctness of programs. As two important parts of program verification, termination proving and safety verification receive more and more
6、 attentions. This thesis performs a systematic and deep study of theories and algorithms for termination proving and safety verification. Main contributions of this thesis can be summarized as follows: 1. Base on the optimization problems, we present a method for generating linear ranking functions.
7、 Firstly, templates of linear ranking functions and a preset range of parameters are given. Secondly, unknown coefficients of templates are replaced by a value of the range. Then considering loop invariants as constraint system and differences of instantiation of linear ranking functions templates a
8、s objective function, we construct an optimization problem. The optimal solution of the optimization problem which is the minimal decending step of ranking functions can be used to compute accurate complexity bound of program. This method for generating linear ranking functions can handle not only l
9、inear and polynomial programs but also some programs with exponents and logarithms. 2. We present a framework of termination proving and safety verification by generation of invariants. Invariants are used as constraint systems of program variables. By instrumenting a counter into loops, we can tran
10、sform the termination problem into an optimization problem. The constraint system of the optimization problem is the invariants set at the exit of the loop. The objective function is computing the minimal value of the loop counter. Using this method, ranking functions are no longer needed and termin
11、ation of some programs without ranking fuctions can also ben proved. We also present a method of verifying safety by proving a logical formula using theorem prover. The logical formula can be constructed from a set of invariants implying a formula which specifies the safety property. Because invaria
12、nts are generated at any control point of a program, weakest preconditions are no longer needed. Compared with methods computing weakest preconditions, our method can be automated more easily. 3. Based on the solving techniques of recurrence equations and optimization problems, we present a practica
13、l approach for computing symbolic complexity bounds of loops. Symbolic complexity bounds of loops, which are upper bounds of iteration times of loops, can be used to measure time complexity and prove termination of loops. Firstly, recurrence equations are generated to specify variables of loops and
14、closed form solutions are computed. Secondly, an optimization problem is constructed which uses closed form solution and negative of loop condition as constraints, uses the variable specifies iteration times of loop as optimization object. Finally, the optimal solution of 国防科学技术大学研究生院博士学位论文 第 iv 页 t
15、he optimization problem is the complexity bound. This approach can prove termination of programs without ranking functions and polynomial loop invariants. Compared with some other works, our approach can get more accurate complexity bounds of loops. 4. Proving conditional termination of programs is
16、the problem to find the preconditions for termination. We present a method of proving conditional termination based on polyranking and constraint solving. For phase- change programs, we can compute the preconditions needed. Compared with another work, our method works more efficiently. Key words： program verification， termination， ranking function， optimization problem，invariants，safety，complexity bound，conditional termination 国防科学技术大学研究生院博士学位论文 第 III 页 表 目 录 表 3.1 实验结果 . 38 表 4.1 CIL/CILi
