| 一个用于指针程序验证的自动定理证明器的设计与实现 |
| |
| 引用本文： | 王振明,陈意云,王志芳.一个用于指针程序验证的自动定理证明器的设计与实现[J].小型微型计算机系统,2010,31(5). |
| |
| 作者姓名： | 王振明 陈意云 王志芳 |
| |
| 作者单位： | 1. 中国科学技术大学,计算机科学技术系,安徽,合肥,230026
2. 中国科学技术大学,苏州研究院,软件安全实验室,江苏,苏州,215123 |
| |
| 基金项目： | 国家自然科学基金，Intel中国研究中心资助项目 |
| |
| 摘 要： | 对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.
|
| 关 键 词： | 指针逻辑 验证条件 自动定理证明器 证明检查算法 |
Design and Implementation of an Automated Theorem Prover Used for Pointer Programs Verification |
| |
| WANG Zhen-ming,CHEN Yi-yun,WANG Zhi-fang.Design and Implementation of an Automated Theorem Prover Used for Pointer Programs Verification[J].Mini-micro Systems,2010,31(5). |
| |
| Authors: | WANG Zhen-ming CHEN Yi-yun WANG Zhi-fang |
| |
| Affiliation: | WANG Zhen-ming,CHEN Yi-yun,WANG Zhi-fang (Department of Computer Science , Technology,University of Science , Technology of China,Hefei 230026,China)(Software Security Laboratory,Suzhou Institute for Advanced Study,Suzhou 215123,China) |
| |
| Abstract: | The increasing demands for high-assurance software make the verification of pointer programs a hot research point. As an extension of Hoare logic,Pointer Logic can be used for accurate pointer analysis of pointer programs. This paper introduces some details in designing and implementing of an automated theorem prover for Pointer Logic,and describes some algorithms. The experimental results show our implementation can fully automatically prove the verification conditions for pointer programs in C-like langua... |
| |
| Keywords: | pointer logic verification condition automated theorem prover proof checking algorithm |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
