| 一个程序验证器的设计和实现 |
| |
| 引用本文： | 张志天,李兆鹏,陈意云,刘刚.一个程序验证器的设计和实现[J].计算机研究与发展,2013,50(5). |
| |
| 作者姓名： | 张志天 李兆鹏 陈意云 刘刚 |
| |
| 作者单位： | 1. 中国科学技术大学计算机科学技术学院 合肥 230026
2. 中国科学技术大学苏州研究院软件安全实验室 江苏苏州 215123 |
| |
| 摘 要： | 形式验证是提高软件可信程度的重要方法,基于逻辑推理对程序性质进行严格的自动证明是当前的研究热点,但尚无可供工业界使用的产品,其根源在于自动定理证明方面的困难.介绍在通过程序分析建立起各程序点的形状图的基础上,如何利用形状图提供的信息来支持程序验证的方法.提出一种利用形状图信息来消除访问路径别名,使得指针程序中非指针部分的性质仍然可以用Hoare逻辑来进行验证的方法,并证明了该方法的可靠性.还提出一种在不使用自定义谓词的情况下,易变数据结构上数据性质的描述和验证方法.另外,介绍所设计并实现的基于上述方法的PointerC语言的程序验证器的原型.它不仅能自动验证操作易变数据结构程序的性质,也能自动验证使用一维数组的程序的性质.
|
| 关 键 词： | 程序验证 Hoare逻辑 形状图逻辑 程序分析 分离逻辑 |
An Automatic Program Verifier for PointerC: Design and Implementation |
| |
| Zhang Zhitian
,
Li Zhaopeng
,
Chen Yiyun
,
Liu Gang.An Automatic Program Verifier for PointerC: Design and Implementation[J].Journal of Computer Research and Development,2013,50(5). |
| |
| Authors: | Zhang Zhitian Li Zhaopeng Chen Yiyun Liu Gang |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
