基于分离逻辑的程序验证方法研究

虽然软件的可信性概念已从以正确性为主要指标扩展到诸如安全、度量等方.面，但正确性仍然是可信软件的重要方面。对实际程序进行正确性检查必然要考虑数据及.数据类型的性质。本项目拟以模型检测方法来自动或半自动验证数据及数据类型性质的正确性，这是软件验证中的关键问题之一。拟采用的技术手段是分离逻辑和实闭域理论，研究如下四个方面的内容：分离逻辑模型、证明系统、分离逻辑公式的模型检验算法和基于C程序的模型抽取方法。为软件验证走向实用迈出坚实的一步，为保障软件的可靠性提供重要的理论方法，对可信软件的设计与开发具有重要理论意义和重大的潜在应用价值.

可信软件的需求加速了程序验证理论和技术的深入发展。人们希望程序验证从理论和技术向实用更进一步推进，希望能够对实际使用的（如程序设计语言C++编写的）程序进行实际验证。本项目正是在这样的背景下提出的。本项目拟以模型检测方法为主来自动或半自动验证数据及数据类型性质的正确性，这是软件验证中的关键问题之一。拟采用的技术手段是分离逻辑和实闭域理论，研究如下四个方面的内容：分离逻辑模型、证明系统、分离逻辑公式的模型检验算法和基于C 程序的模型抽取方法。项目取得的主要成果包括：（1） 为分离逻辑验证建立了多种模型，特别是实数模型和概率迁移系统模型，实数模型将原来分离逻辑模型从整数论域扩展到实数模型，使得分离逻辑能够描述更多、更实用的数据类型；概率模型的建立使得分离逻辑能够更加实用化；（2）给出了基于上述两种模型的分离逻辑模型检查算法或直接验证算法；（3）初步建立了程序运行系统的分析与验证方法。在重要会议和杂志发表论文？篇，完成了预订的研究任务，基本达到了预订的研究目标。取得的成果为软件验证走向实用迈出坚实的一步，为保障软件的可靠性提供重要的理论方法，对可信软件的设计与开发具有重要理论意义和重大的潜在应用价值.