面向程序验证的自动定理证明理论、方法与工具研究

Automated theorem proving is an important research field crossing the studies of computer science and mathematics, and plays a major role in the verification of programs and hybrid systems. Nowadays, the research in its theory, method and application is highlighted in both academia and industry, whilst facing a large number of challenges. This project is motivated by practical requirements in program verification and centers on three key scientific problems, i.e. the decision problems of non-polynomial theories, efficient algorithms in complex combined theories, and reachability analysis of programs and hybrid systems. The project aims to make progress in three aspects. First, we are trying to solve several fundamental problems in the theory of automated theorem proving, such as the decision problems of combined theories, efficient decision methods for non-linear formulae, the decision problems of non-polynomial theories and Craig interpolants construction for non-linear formulae. Second, we aim at discovering efficient methods in automated theorem proving for several basic problems in the verification of programs and hybrid systems, for instance, complete methods for generating equality-type invariants for polynomial programs, termination analysis of programs based on k-induction, and the fixed-point problem of reachability analysis of hybrid systems. Finally, the newly designed algorithms will be implemented and integrated into our previous tools and further applied to the analysis and verification of airborne software. The application team features great interdisciplinarity and has been cooperating well for a long time. We believe we would make progress in the research of the aforementioned problems in the theory and method of automated theorem proving, and facilitate the verification and analysis on airborne software.

自动定理证明是计算机科学和数学交叉的一个重要研究领域，是程序和混成系统分析与验证的重要技术，其理论、方法和应用研究是学术界和工业界关注的热点，面临诸多挑战。本项目从程序验证的实际需求出发，围绕非多项式理论判定、复杂混合理论高效求解、程序和混成系统可达性分析三个关键科学问题，拟开展三个方面的研究：一，自动定理证明中的基本问题，包括：混合理论判定问题，非线性公式高效判定方法，非多项式理论判定问题，非线性公式的Craig插值问题；二，程序和混成系统验证中与自动定理证明相关的几个基本问题，包括：等式型不变量的完备生成方法和基于k-归纳的程序终止性分析，混成系统可达集计算中的不动点问题；三，相关工具开发和面向机载软件的案例研究。我们是一个跨学科的申请团队，有很好的研究基础和多年卓有成效的合作，可望在上述自动定理证明理论和方法的研究中取得突破，并将新的理论和方法应用于机载软件中关键系统的验证和分析。

对诸如航天器、飞机、高速列车、核反应堆等复杂安全攸关系统控制软件的功能和信息安全验证是具有国家战略需求性质的重大问题。自动定理证明作为程序和混成系统分析与验证的重要技术，其理论、方法和应用研究是学术界和工业界关注的热点，面临诸多挑战。. 根据项目计划书的安排，项目组从程序和混成系统验证的实际需求出发，围绕自动定理证明中的基本问题、程序和混成系统验证中与自动定理证明相关的几个基本问题以及相关工具开发和面向机载软件的案例研究三个方面，对以下九点内容：A.混合理论判定问题，B.非线性公式高效判定方法，C.非多项式理论判定问题，D.非线性公式的Craig插值生成问题；E.等式型不变量的完备生成方法和基于k-归纳的程序终止性分析，F.循环和递归程序总结生成问题，G.混成系统可达集计算中的不动点问题；H.相关工具开发，I.面向机载软件的案例研究，开展了系统全面的研究。. 项目组全面完成了研究目标。在理论和算法研究中取得多项重要进展，尤其在非线性公式的Craig插值、非线性公式高效判定方法、非多项式理论判定以及程序和混成系统可达性分析等问题的研究上取得的部分结果是目前最好的理论或算法结果。例如：我们得到了非线性理论Craig插值生成目前最好的理论结果；证明了一类混合三角多项式约束可判定；给出了目前最弱的栅栏函数条件，能生成更多的栅栏函数；得到了关于混成系统可达集计算问题最好的判定结果。在工具开发方面，实现了混成系统建模、分析和验证工具链MARS 2.0版本。与MARS之前的版本相比，它支持混成系统更多的功能特征以及对这些复杂行为的仿真检查，并基于定理证明在Isabelle中完全实现了混成系统的验证，实现了从验证后的抽象模型到可靠的C代码的自动生成；开发了非线性理论SMT原型求解器LiMbS，为进一步开发自主可控的高效SMT求解器打下了基础。在案例研究中，除完成计划书设定的两个验证案例外，还针对国家某重大战略型号核心操作系统内核的任务管理和调度、任务同步与通信、核间通讯等关键模块和功能进行了验证。