【作者】 田丰；

【导师】 邓胜兰；

【作者基本信息】 国防科学技术大学 ， 计算机技术， 2011， 硕士

【摘要】 随着计算机科学的高速发展,软件在人们日常生活中扮演着越来越重要的角色,软件程序的正确性验证研究成为学界高度关注的课题。程序的停机性和安全性验证是程序正确性验证中的两个重要内容,本文基于Mathematica和构造程序不变式,设计并实现了程序的停机性和安全性验证工具,主要工作包括以下几个方面:1.程序不变式自动构造工具的实现。基于Mathematica平台,设计了一个程序不变式自动构造工具。其中,线性不变式的构造采用CILinear,多项式循环不变式的构造采用Aligator。构造的不变式描述了循环程序变量间的关系,为程序正确性验证提供了计算基础。2.停机性验证。首先在程序循环点插桩循环计数器记录循环次数,然后构造程序不变式集作为最优化问题的约束系统,并以循环计数器是否存在最小值为最优化问题目标,将停机性验证问题转化为最优化问题,基于Mathematica提供的最优化问题求解函数Minimize,有效实现了程序的停机性验证,而且可以生成精确的循环符号化复杂度上界。3.安全性验证。首先标注出程序的前后置断言,建立安全性验证命题,用构造出的不变式集形成验证条件,将安全性验证问题转化为使用定理证明器验证不变式集是否蕴含安全性逻辑公式的问题,然后基于定理证明器Theorema中的验证工具PCS,有效实现了程序安全性验证工作。更多还原

【Abstract】 With the rapid development of computer science, software plays an increasingly important role in people’s daily life, so the correctness verification of software program got a great deal attention in academic domain. Termination and safety verification are two important parts of program correctness verification, based on Mathematica and generation of invariant, we design and implement a tool for termination and safety verification. The main contributions are summarized as follows:1. The implementation of automatic program invariants generation. Based on Mathematica, we have designed and implemented a tool for automatic program invariant generation, which constructs the linear invariants using CILinear and constructs the polynomial loop invaraints using Aligator. The constructed invariants describe the relationships among the loop program variables, and provide the computation basis for the program correctness verification.2. The implementation of termination verification. First we instrument a counter into program loop to record loop times. Then constructed invariant sets as constraint system and whether counter have minimum as objective function, we transform the termination verification problem into an optimization problem, based on the optimization problem-solving function Minimize in Mathematica, we can not only effectively complete the termination verification, but also generate the exact complexity bound of program loops.3. The implementation of safety verification. First we instrument the assume and statements, establish the propositions for safety verification, construct the verification conditions with the set of invariants, transform the verification of safety into the verification of the validity of the logic formula that the invariants imply the the propositions characterizing safety. Then based on the theorem prover PCS in Theorema, the logical formula can be constructed from a set of invariants implying a formula which specifies the safety property. We can effectively implement the safety verification of program.更多还原