-
题名一个程序验证器的设计和实现
被引量：10
- 1
-
-
作者
张志天
李兆鹏
陈意云
刘刚
-
机构
中国科学技术大学计算机科学技术学院
中国科学技术大学苏州研究院软件安全实验室
-
出处
《计算机研究与发展》
EI
CSCD
北大核心
2013年第5期1044-1054,共11页
-
基金
国家自然科学基金项目(61170018
61003043)
-
文摘
形式验证是提高软件可信程度的重要方法,基于逻辑推理对程序性质进行严格的自动证明是当前的研究热点,但尚无可供工业界使用的产品,其根源在于自动定理证明方面的困难.介绍在通过程序分析建立起各程序点的形状图的基础上,如何利用形状图提供的信息来支持程序验证的方法.提出一种利用形状图信息来消除访问路径别名,使得指针程序中非指针部分的性质仍然可以用Hoare逻辑来进行验证的方法,并证明了该方法的可靠性.还提出一种在不使用自定义谓词的情况下,易变数据结构上数据性质的描述和验证方法.另外,介绍所设计并实现的基于上述方法的PointerC语言的程序验证器的原型.它不仅能自动验证操作易变数据结构程序的性质,也能自动验证使用一维数组的程序的性质.
-
关键词
程序验证
hoare逻辑
形状图逻辑
程序分析
分离逻辑
-
Keywords
program verification
hoare logic~ shape graph logic
program analysis
separation logic
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名一种用于指针程序的形状分析方法
被引量：1
- 2
-
-
作者
刘刚
胡凯平
宋发兴
-
机构
中国人民解放军
-
出处
《计算机与现代化》
2012年第4期82-85,共4页
-
文摘
指针程序的分析一直是研究热点。本文提出一种基于形状图逻辑的形状分析方法,其中形状分析采用形状图来表达程序中指针的指向和相等关系,并用形状图逻辑来进行推理。形状图逻辑是一种把形状图看成有关指针的断言,并在此基础上对Hoare逻辑进行扩展而得到的程序逻辑。首先介绍所提出的形状图和形状图逻辑;然后在此基础之上,设计一种基于形状图逻辑的形状分析方法。
-
关键词
形状图
形状图逻辑
hoare逻辑
形状分析
程序分析
-
Keywords
shape graph
shape graph logic
hoare logic
shape analysis
program analysis
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名一种验证指针程序的方法
被引量：1
- 3
-
-
作者
张志天
陈意云
刘刚
-
机构
中国科学技术大学计算机科学与技术学院
中国科学技术大学苏州研究院软件安全实验室
-
出处
《微型机与应用》
2011年第16期9-11,共3页
-
文摘
利用形状图逻辑和形状系统来解决指针程序的分析和验证中的困难。该方法要求程序员声明各种递归结构体类型参与构建的数据结构的形状,并声明指针变量所指向的形状,以便程序分析工具能建立各程序点的形状图,并以此来支持程序验证。探讨了在指针相等关系静态可确定的情况下,避免在Hoare逻辑上做复杂扩展的指针程序验证方法。
-
关键词
hoare逻辑
形状图逻辑
程序分析
分离逻辑
-
Keywords
hoare logic
shape graph logic
program analysis
separation logic
-
分类号
TP311.1
[自动化与计算机技术—计算机软件与理论]
-
