| 用于指针逻辑的自动定理证明器 |
| |
| 引用本文： | 王振明,陈意云,王志芳.用于指针逻辑的自动定理证明器[J].软件学报,2009,20(8):2037-2050. |
| |
| 作者姓名： | 王振明 陈意云 王志芳 |
| |
| 作者单位： | 1. 中国科学技术大学,计算机科学技术系,安徽,合肥,230026
2. 中国科学技术大学,苏州研究院,软件安全实验室,江苏,苏州,215123 |
| |
| 基金项目： | Supported by the National Natural Science Foundation of China under Grant Nos.60673126, 90718026 (国家自然科学基金) |
| |
| 摘 要： | 提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL 的工具中得以实现.APL 自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自动定理证明器.
|
| 关 键 词： | 指针程序 指针逻辑 验证条件 自动定理证明器 证明检查器 |
| 收稿时间： | 2008/5/25 0:00:00 |
| 修稿时间： | 2008/10/9 0:00:00 |
Automated Theorem Prover for Pointer Logic |
| |
| WANG Zhen-Ming,CHEN Yi-Yun and WANG Zhi-Fang.Automated Theorem Prover for Pointer Logic[J].Journal of Software,2009,20(8):2037-2050. |
| |
| Authors: | WANG Zhen-Ming CHEN Yi-Yun and WANG Zhi-Fang |
| |
| Affiliation: | Department of Computer Science and Technology;University of Science and Technology of China;Hefei 230026;China;Software Security Laboratory;Suzhou Institute for Advanced Study;Suzhou 215123;China |
| |
| Abstract: | This paper presents a technique for designing theorem prover which mainly based on transformation
and substitution for Pointer Logic. The technique realized as a tool called APL is implemented. The APL theoremprover is fully automated with which proofs can be recorded and checked efficiently. The tool is tested on pointerprograms mainly about singly-linked lists, doubly-linked lists and binary trees. |
| |
| Keywords: | pointer program pointer logic verification condition automated theorem prover proof checker |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
