面向软件演化的回归形式化验证研究

The development of modern software cannot be accomplished in an action, but needs an incremental and evolving procedure. It is important to develop efficient techniques to formally verify evolving software systems. Regression formal verification is being considered as a promising approach for this purpose. This technique is still new and remains challenging. It is valuable both to theory and practice. This project mainly addresses the following techniques: regression model checking, regression compositional verification and regression program analysis. The project will develop a regression verification tool for evolving software systems, which will be applied to the verification of driver programs.

现代软件的开发已经不再是一蹴而就式，而是生长演化式的。适应于软件的持续改变与演化，开发高效的形式化验证技术具有重要意义。回归形式化验证是应对这一问题的有效途径。该技术的研究在国际上仍是崭新且富有挑战性的，具有重要的理论与应用价值。本课题拟开展回归模型检测、回归组合验证和回归程序分析的研究。以此为基础设计面向软件演化的回归验证工具，并在驱动程序验证中进行应用。

现代软件的开发已经不再是一蹴而就式，而是生长演化式的。适应软件的持续改变与演化，开发高效的形式化验证技术具有重要意义。本课题研究面向软件演化的回归形式化验证技术，首次提出了增量式程序终止性证明和回归组合验证的想法；设计并实现了增量式程序抽象和增量式程序分析等回归验证技术。此外，在程序验证的硬核问题（循环不变式生成、终止性证明、约束求解）上也取得了重要进展。基于上述成果，开发了程序验证工具Ceagle，并在驱动程序验证中进行了应用。