构建高可信软件中的自动定理证明问题研究

关键软件的高可信性质显得越来越重要。程序验证并携带证明是提高软件可信性的一种重要方法。然而目前高可信软件开发中的验证条件证明大都采用手工完成，工作量巨大，制约了程序验证的实用性。现有的通用定理证明器在自动性、证明输出形式等方面并不能满足携带证明的代码开发的需要。.在系统程序开发中针对各领域特定问题而设计的论域专用逻辑，可以避免设计一种通用逻辑的困难，从而克服现阶段证明难以自动完成的问题。积累各论域专用逻辑的自动定理证明技术是最终达到自动程序验证的希望之路。本课题研究面向论域专用逻辑的自动定理证明技术和输出简洁、严格证明的一般方法。探索系统程序验证中形式表达程序性质、构建引理库、证明策略库的规律和方法。本课题研究目标是完成论域专用逻辑的定理证明关键技术，并开发出实用的自动定理证明工具，结合一个出具证明编译器展示其应用前景，对于将携证明的代码技术推向实用具有一定的理论价值和科学意义。

关键软件的高可信性质显得越来越重要。程序验证并携带证明是提高软件可信性的一种重要方法。然而目前高可信软件开发中的验证条件证明大都采用手工完成，工作量巨大，制约了程序验证的实用性。..在系统程序开发中针对某一领域特定问题而设计的论域专用逻辑，可以避免设计一种通用逻辑的困难，从而克服现阶段证明难以自动完成的问题。我们为推理操作堆上易变数据结构的串行C指针程序设计了形状图逻辑（Shape Graph Logic），为操作系统验证设计了较小C子集C3及其程序逻辑。此外，积累各论域专用逻辑的自动定理证明技术是最终达到自动程序验证的希望之路。本课题研究面向论域专用逻辑的自动定理证明技术和输出简洁、严格证明的一般方法。我们给出了线性整数、分类逻辑（片断）定理证明器及其证明项生成的方法。我们通过程序验证器、出具证明编译器、验证条件生成器等工具原型，结合开发出实用的自动定理证明工具，展示定理证明技术的应用前景，为未来构建高可信系统软件积累了一定的研发经验。目前我们实验室正在使用这些前期设计的逻辑和证明方法来验证一个小型实际的操作系统μC/OSII...此外，除了程序验证领域，程序分析领域也需要定理证明技术作为精确分析的支撑。在一些安全攸关领域（金融，电力，通信等），程序验证代价相对较高并不能在短期内大规模推广。而程序分析代价较低，能够以较低的代价较早地发现代码中的潜在错误。而通常的程序分析精度低，误报和漏报较为严重，而较为精确的方法通常依赖于约束求解器或者自动定理证明器。为了展示我们在定理证明方面的相关研究成果，我们项目组正在将相关的工作经验用于一个较为精确报告错误的C程序静态分析工具，并期望能够在三到五年内实现工具的产品化。