在信息时代,计算机软件技术得到了广泛的应用。然而,随着软件功能越来越强大,软件本身也变得愈发复杂,软件的可靠性和安全性越来越难以得到保障。在通常使用的C,C++或者Java语言中,为了使程序能够高效运行,指针或者引用在程序中大量使用。但是指针的灵活使用很容易引起错误,比如空指针或者悬空指针引用,内存泄露等。这些错误不仅难以发现,如果一旦发生可能导致系统崩溃。而且,这些程序漏洞可能被黑客加以利用。另一方面,指针错误之所以难以被发现,是因为不同指针之间存在可能的别名关系,即是两个语法上不同的名字在运行的时候可能引用同一个内存地址。修改一个名字对应的值,别的名字所对应的值可能也会随之改变,给程序调试和程序推理带来很大的困难。因此,带有指针程序的安全性在软件安全研究中占有重要位置。由于指针程序安全研究具有很大的挑战性,工业界常用的软件测试方法无法完全保证错误不会发生,因而指针程序性质证明方法成为当前研究热点。而现有的证明方法,要么需要显式引入堆或栈等高级语言语法之外的概念来刻画程序的运行状态,要么生成的验证条件太过于复杂而不能够自动证明,而需要程序员手工证明。堆和栈的描述需要知道确切的内存地址,但是具有同构结构的堆是不可以区分的。而无存储模型方法则克服了上述所有困难,不需要显式引入堆栈概念,而其良好性质保证可以被自动机实现,因而证明可以自动。指针逻辑在本质上是基于无存储模型方法,但是当前还具有很多不足。当前指针逻辑缺少抽象模型描述,导致了指针逻辑规则都是由算法风格函数辅助构成,这使得难以看清楚指针逻辑本质。而且,当前指针逻辑支持的指针特征较少,虽然断言语言支持符号访问路径,用户自定义谓词和描述性谓词,但是其实现PLCC(V1)(Pointer Logic Certifying Compiler,简称为PLCC,V1表示Version 1,后面的V2表示Version 2)的推理并不支持。最重要的是,PLCC(V1)生成的验证条件并不能自动证明,而需要程序员通过交互式定理证明器COQ来完成证明。基于上述考虑,本文在访问路径相等概念上提出一个无存储模型,研究了该模型的各种性质,例如右规则性,前缀闭包性等。同时,本文专注于无存储模型上的指针逻辑断言的良型性,继而重新阐述了指针逻辑推理规则。为了使指针逻辑能够验证更大范围的程序,本文提出了针对指针逻辑的框架规则(frame rule)和函数调用规则。此外,本文在原有指针逻辑基础上,扩展源语言和断言语言来支持指针算术,然后在方便模块化实现前提下扩展指针逻辑规则来保障指针算术的安全。原来指针逻辑中的集合是无名集合,而无名集合不能处理含有某些情况下的函数调用的程序,因而本文提出带标签的集合可以适用于任意函数调用的验证。在实现方面,本文根据无存储模型性质设计了实现指针逻辑规则的自动推理算法,并提出了展开机制来处理断言语言支持用户自定义谓词和描述性谓词。最后,本文工作均在PLCC(V2)的前端中实现。本文的主要特色和贡献为:●本文提出了一个比已存在无存储模型更有效更简洁的无存储模型。此模型不仅继承了已存在无存储模型的优点,而且克服了其冗余多,表示代价高的缺点。●本文完善了指针逻辑,在抽象模型上以一种简单更为容易理解的方式重新阐述指针逻辑推理规则。由于抽象模型没有传统无存储模型的冗余,花费代价大等缺点,因而本文可以发现以前指针逻辑(Chen et al.,2007a,b)规则中具有一个漏洞:以前指针逻辑所定义的no_leak函数在某些时候会将某些正确程序误认为会出现内存错误而拒绝。本文给出修正此漏洞的规则,同时这也反映了建立抽象模型的必要性,因为以前的指针逻辑规则是基于一些复杂的算法风格的辅助函数,并且导致难以看清楚指针逻辑的本质。●本文扩展了指针逻辑。相比扩展前的指针逻辑,本文扩展了指针逻辑在局部推理的规则、扩展支持在动态数组上的指针算术以及利用带标签的集合来验证任意函数调用的扩展,这样指针逻辑就能够在更大范围内保障程序的安全。●本文设计了实现指针逻辑规则的算法和提出了展开技术来实现谓词推理自动化,并将其应用到自动验证工具PLCC(V2)前端实现上。相比PLCC(V1)需要程序员利用COQ手工证明其生成的验证条件,PLCC(V2)可以自动完成各种推理证明而不需要程序员手工干预。同时而可以利用谓词展开技术验证很多非平凡的指针程序,例如在单向链表,双向循环链表,树等常用数据结构上的操作,其中包括被认为是指针形式化指标的Schorr-Waite树遍历算法。