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

项目名称： 基于分离逻辑的程序验证方法研究

项目编号： No.61170299

项目类型： 面上项目

立项/批准年度： 2012

项目学科： 自动化技术、计算机技术

项目作者： 王捍贫

作者单位： 北京大学

项目金额： 52万元

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

中文关键词： 分离逻辑；概率迁移系统；模型检查；；

英文摘要：

英文关键词： Separation Logic；Probabilistic Transition System；Model Checkong；；