重写系统的基础理论及其在软件质量保障中的应用

While information technologies become ubiquitous in our daily life, the quality of software systems has been closely related to the safety of our lives and properties. Thanks to its rigorous and mathematical characteristics, formal methods become one of the key techniques to verify the correctness of software. As one of the most popular verification techniques, theorem proving is difficult for non-experts to use though. Thus its widespread application in industry is hindered. Aiming at improving the user-friendliness of theorem provers, this project is devoted to the investigation of the methods for checking confluence of rewrite systems, which are the underlying models within theorem provers. We will develop theories, based on the decreasing diagrams framework, to check the confluence of non-left-linear higher-order systems without termination assumptions. These methods will lay a theoretical foundation for the user-defined feature for theorem provers. Besides, starting with the verification of scheduling modules, we will explore more ways of applying rewriting techniques to formal verification, thus to the advancement of software quality assurance.

随着信息技术逐渐渗入人们的生产生活中，软件系统质量变得与人们的生命财产安全息息相关。形式化验证技术以其严谨性与高度数学化的特点，已成为保障软件正确性的关键技术。定理证明技术作为主流验证技术之一，“难学难用”却阻碍了它在工业界的大规模应用。为了提高定理证明器的用户友好性，本项目拟开展针对其底层理论模型——重写系统的合流性证明技术的研究，基于递减图框架开发能适用于非左线性、非终止高阶系统的合流性证明理论，为定理证明器的用户可定制特性奠定理论基础。同时，以调度模块的验证为切入点，本项目将探索重写系统在形式化验证技术其它方面应用的可能性，进一步推进形式化验证技术在软件质量保障过程中的应用。

现代软件已经成为人们生活的一部分，软件系统质量变得与人们的生命财产安全息息相关。由于现代软件的高度复杂性，传统的软件测试技术已无法满足诸如自动驾驶、加密支付等安全攸关场景的需求。因此，更可靠的形式化验证技术逐渐成为软件正确性保障的关键技术。本项目的研究目标是对形式化验证系统的底层模型之一——重写系统的理论难题进行探索；另一方面，针对特定领域，研究重写技术在相关形式化验证技术中的应用。本项目着重研究了以下内容：左线性非终止高阶重写模型的合流性及其证明技术；C语言密码程序的正确性及其自动化验证技术；API调用错误在大规模软件中的检测技术；可满足性模理论约束求解器的正确性保障技术；以及神经网络鲁棒性的自动验证技术。在实施过程中，本项目提出了一套针对C语言密码程序正确性的自动化验证方法；设计了一种领域特定语言及相关的静态分析工具，用于自动检测C代码中的API调用错误；开发了一个位向量理论的约束求解器，并对它的正确性提供了可检查的证明。每项工作不仅具备理论突破点，而且均有相应的工具实现和应用。项目的研究成果有效保障了C语言密码库的安全性，而且也进一步提高了基于约束求解器的诸多形式化验证技术与工具的可靠性。