随着计算机学科的迅猛发展，计算机软件正逐渐演化成为人们学习生活中的一个庞大的体系。另一方面，软件的安全形势非常严峻，尤其随着移动计算的日益普及，对未受信源提供代码的安全执行问题也慢慢浮现出来。软件的安全性成为关注的重点，在软件安全性的研究中，软件满足特定安全策略的证明方法是目前国内外研究的热点之一。　　 出具证明编译器是软件安全的一个重要研究方向，程序员在源码上添加其属性描述形成程序规范，验证条件生成器对程序规范推理演算生成验证条件，接着由自动定理证明器对验证条件求解并生成证明，最后将编译器将生成的可执行文件与证明并输出，代码消费方可以使用自己信任的证明检查器来检查该证明的正确性。不难发现，自动定理证明器在出具证明编译器内部发挥了非常重要的作用。　　 CComp是我们实验室先前的一个研究项目，是一个能证明部分指针程序正确性的出具证明编译器。在先前工作的基础上，本文在其源级做了扩展，通过添加自定义谓词机制来增强断言语言的表达能力。用户通过定义一些谓词来帮助描述程序的归纳性质，并且通过提供这些谓词所满足性质的等式，来支持出具证明编译器自动完成这些程序性质的证明。这意味着出具证明编译器可以证明的性质将更加丰富灵活。　　 本文的研究内容主要有：为添加的自定义谓词机制重新设计断言语言，要求断言语言是基于分离逻辑设计的，并且为项目组所设计的出具证明编译器补充设计并实现一个自动定理证明器，以支持自定义谓词。本文的贡献是解决了如何利用用户提供的谓词定义及相关引理，依据特定的推理规则，形成自动定理证明算法的问题。　　 本文首先介绍了本课题的研究背景和研究现状，接着简单介绍了本课题的项目基础CComp及其流程。本文接着介绍了源级框架下的程序规范，验证条件生成器依据程序语义对程序推理生成验证条件，断言语言上的推理规则，支持自定义谓词及相关引理的自动定理证明器等。最后介绍了两个证明实例和总结。　　 本文工作的意义在于，通过对支持用户自定义谓词的出具证明编译器中自动定理证明搜索策略的探索研究，扩展了出具证明编译器规范的表达性，程序员能够以此来表达更复杂的程序性质。同时在这个过程中，积累了自动定理证明技术在多理论整合和专用逻辑方面的研究经验，为程序验证的相关研究提供了技术支持与理论基础，提高了高可信软件的开发效率。