一个用于指针程序验证的自动定理证明器的设计与实现

摘要：

对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.

关键词：指针逻辑、验证条件、自动定理证明器、证明检查算法

所属期刊栏目：31

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金项目60673126,90718026;Intel中国研究中心资助项目

在线出版日期：2010-06-21（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：801-806