随着信息时代的到来和深入，计算机技术已经在各行各业中得到了广泛地应用。但随着计算机软件系统的普及和规模的不断增大，其安全性问题也越来越突出。提高软件可靠程度的方法有很多，形式程序验证是其中一个重要的方法。基于逻辑推理是程序验证中最严格也最可靠的，它根据特定的程序逻辑通过形式化的数学推导演算，并利用定理证明工具来证明。但由于自动推断循环不变式困难、断言语言表达力弱以及自动定理证明能力有限等诸多原因，形式程序验证尚未在工业界得到应用。　　 本文的工作建立在一个基于形状图逻辑的自动程序验证原型系统上，主要用于指针程序的验证。该验证过程主要分成两个阶段:第一阶段是对指针程序进行形状分析，第二阶段是利用形状分析得到的结果进行程序验证。其中，形状分析阶段使用形状图逻辑和形状系统，实现了循环不变形状图的自动推断，并且对于非递归函数可以推断出函数前后形状图。　　 本文主要的研究工作是形状图理论的定理证明及其在指针程序验证中的应用。形状图理论主要包括形状图重写系统、形状图等价判定方法和形状图蕴涵判定方法;形状图理论在指针程序验证中的应用主要包括对循环不变形状图和递归函数前后形状图的推断。通过对系统原型做扩展之后，系统能够验证带递归的指针程序。　　 本文的主要贡献是:　　 第一，设计并实现了形状图理论的判定方法。　　 形状图及其等价变换规则和蕴涵变换规则可分别类比为代数项及其等式规则和重写规则，因而可像研究代数规范的理论那样来研究形状图理论。我们定义了形状图重写系统及其终止性、局部合流性和合流性等概念，最后得到基于形状图重写的形状图等价判定和蕴涵判定的方法。　　 第二，设计并实现了指针类型递归函数前后形状图的自动推断方法。　　 该自动推断方法源子一个通过迭代推断循环不变式的一般方法，并借助了上述形状图理论的判定方法。该方法的实现使得原型系统能够用于指针类型递归程序验证。　　 通过上述方法的实现以及对系统原型其他地方的完善，系统原型能够验证平衡二叉排序树和自顶向下伸展树等复杂的易变数据结构的程序。