学位论文 > 优秀研究生学位论文题录展示

基于不变式的程序验证工具的设计与实现

作　者: 田丰
导　师: 邓胜兰
学　校: 国防科学技术大学
专　业: 计算机技术
关键词: 程序验证停机性安全性不变式最优化问题复杂度上界
分类号: TP311.11
类　型: 硕士论文
年　份: 2011年
下　载: 21次
引　用: 0次
阅　读: 论文下载

内容摘要

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

基于不变式的程序验证工具的设计与实现

内容摘要

全文目录

相似论文