用于指针逻辑的自动定理证明器(英文)

作     者：王振明 陈意云 王志芳 WANG Zhen-Ming;CHEN Yi-Yun;WANG Zhi-Fang

作者机构：中国科学技术大学计算机科学技术系安徽合肥230026 中国科学技术大学苏州研究院软件安全实验室江苏苏州215123 

基　　金：Supported by the National Natural Science Foundation of China under Grant Nos.60673126 90718026~~ 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2009年第20卷第8期

页      码：2037-2050页

摘      要：提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL的工具中得以实现.APL自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自动定理证明器.

主 题 词：指针程序 指针逻辑 验证条件 自动定理证明器 证明检查器 

学科分类：08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 081202[081202] 

核心收录：

D　O　I：10.3724/sp.j.1001.2009.00572

馆 藏 号：203110224...