对高可信软件需求的增加使得指针程序的验证成为近十几年的研究热点,自动定理证明作为形式化方法之一,在软件验证和程序分析工具当中发挥着及其重要的作用。然而,自动定理证明本身是一个非常难于解决的问题,尤其是待解决的问题中存在着指针以及涉及到指针的递归定义的谓词的情况下。考虑到以上问题,我们在一个出具证明编译器框架中设计并实现了一个自动定理证明器和一个起辅助作用的证明检查器,来帮助完成指针程序的验证。实验结果证明,我们的实现不但具有创新性而且具有实际可行性。在本文中,我们首先介绍了项目的研究背景和理论基础,然后提出了一种为指针逻辑来设计自动定理证明器的新技术,这项技术主要是基于变换和替代,我们已经在一个被称为APL的工具中实现了该技术。指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析。此外,本文还介绍了APL自动定理证明器的详细设计和实现,描述了一些关键算法,比如指针逻辑决策过程,整型线性算术决策过程,证明检查算法等等。APL定理证明器是完全自动的,并且APL所产生的证明可以被有效的记录和检查。在出具证明编译器PLCC 2中,我们调用了APL自动定理证明器,并对一些具有代表性的程序进行了测试。实验结果表明,APL完全可以自动地证明使用类C语言编写的关于单链表,双链表和二叉树的指针程序。本文的主要特色和贡献为:1.提出了一种为指针逻辑设计自动定理证明器的新方法。该方法是为了解决基于指针信息集合表示的验证条件的证明问题而设计的。在实现时我们使用了替代,变换,指针分析等基本技术,在指针信息集合上完成各种推理和证明。并且我们使用这种方法为指针逻辑实现了一个完全自动的定理证明器。这在已存在的比较流行的定理证明器中是不曾实现过的。2.设计了指针逻辑的断言语言和相应的断言演算。该断言语言能够以简洁易懂的形式描述指针逻辑的最显著的特点,主要使用指针信息集合的形式表示待验证的指针程序在各程序点上的状态。断言语言和断言演算是定理证明器和证明检查器设计和实现的基础。3.设计了一个证明检查算法,并在一个证明检查器中实现了该算法。该算法不同于已有的证明检查算法之处在于,它主要是使用模式匹配的方法对以指针信息集合表示为主的证明进行快速有效的检查,来保证证明的正确性。4.实现了一个用于指针逻辑的自动定理证明器。该实现主要包含指针逻辑和整型线性算术两大理论的决策过程,独创的验证条件检查器,证明生成、保存和检查模块等。可以完全自动地证明出具证明编译器PLCC所产生的关于单链表,双链表和二叉树等程序实例的验证条件。APL自动定理证明器的实现,使得出具证明编译器PLCC 2不再需要依赖交互式证明工具Coq,能证明更多的、规模更大的程序实例,整个工具的功能因此变得更加强大。