程序验证用逻辑证明的方法证明程序满足其规范，是实现安全性的重要方法。出具证明编译器(Certifying Compiler)是编译器与验证器的结合。本文描述的出具证明编译器项目CComp让用户给出描述程序正确性的规范，并在源代码使用霍尔逻辑风格的推理规则产生验证条件(Verification Condition，VC)，经由证明器证明后产生证明项。然后将源代码和规范转化成底层的汇编代码和其上的规范，并利用源级证明项生成汇编代码级证明，最终生成携带证明代码。 　　 CComp由多人协作完成，本人承担项目中的断言语言设计以及验证条件生成和化简工作。实验室先前的项目PointerC[4]，过大的验证条件规模成为系统性能的瓶颈。因此CComp采用一系列的措施来化简VC，删除其中的冗余。　　 实用的编译器会包含众多优化，以提高程序执行的效率。编译优化是一系列程序变换，对于出具证明编译中包含规范的程序，变换前的程序的规范可能无法正确或充分地描述变换后的程序，为此程序规范也应该随着代码优化一起转换。目前关于出具证明编译器的项目较少研究编译优化的影响，但编译优化是决定出具证明编译器是否能走向应用的关键因素之一。　　 本文通过分析研究，针对以上两个重要问题分别提出了相应的解决方案，并实现了原型系统验证方法的合理性。本文的主要贡献为：　　 1.为CComp项目设计了使用分离逻辑描述的断言语言和其推理规则，实现了相应的验证条件生成器；设计并实现了一个重写系统，实现了验证条件的化简，解决了验证条件过大的问题。　　 2.通过研究数据流优化的基本行为，实现了一个包含多种优化和相应规范转换的编译器原型系统，利用数据流分析结果来变换规范，使各循环的循环不变式经过调整后，能作为优化后程序的相应循环的循环不变式。并初步总结出了通用的转换模式。　　 本文第一部分工作是CComp项目的一部分。第二部分工作则较为独立，可作为未来对包含代码优化的出具证明编译器的研究基础。