当今社会，计算机安全问题的严峻形势使得人们迫切需要高可信软件。形式化验证方法是提高软件可信度的一种可靠的方法，其中基于演绎推理的的方法更是近些年来的研究热点。　　本实验室基于演绎推理方法设计并实现了一种形式化程序验证的工具——面向PointerC的程序验证原型系统（简称原型系统）。它是一个源码级的程序验证工具，其特色是先通过形状分析得到指针之间的关系，然后根据Hoare逻辑的扩展对程序进行演绎推理并生成验证条件，最后交给自动定理证明器证明。　　然而自动定理证明器对于本原型系统来说具有两点能力不足，第一点是无法进行归纳证明，第二点是无法自动发现全称量词彼此之间的联系。本文针对这两个问题，在实验室原有的工作基础上对原型系统的功能进行改进。　　本文的主要贡献如下:　　第一，设计并实现对程序员提供的性质定理的自动归纳证明。为了提高断言语言的表达能力，原型系统引入自定义归纳谓词。程序员有时在编写程序代码的过程中，会利用到递归定义谓词的归纳性质。同时，由于自动定理证明器在证明验证条件的过程中无法推导出这些归纳性质，程序员需要给出相关的性质定理辅助自动定理证明器证明。为了保证性质定理的正确性，本文给出了对性质定理先进行分析后进行结构归纳的方法，实现了性质定理的自动证明。　　第二，改进了带有全称量词断言的程序验证功能。当验证条件中包含全称量词断言时，自动定理证明器会因为无法发现多个全称量词彼此之间的关系而证明失败。本文提供了一种结合形状图对全称量词断言分组的思路，并且依据这种思路对验证条件中出现的全称量词进行处理，从而使得原型系统可以通过验证条件中包含多个全称量词断言的程序的验证。　　本文对原型系统进行扩展后，解决了当前原型系统中因为自动定理证明器两点能力不足带来的问题。保证了程序员提供的性质定理的正确性，不仅使得之前所有操作易变数据结构的程序实例的验证结果更加可靠，还使得原型系统可以验证包含多个全称量词断言的程序。