欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
位置：立项数据库 > 立项详情页
中文摘要：
软件形式化验证是国际计算机科学基础研究的前沿领域之一，基于抽象模型检测方法是当前软件形式化验证的研究热点。本项目将抽象解释、模型检测和定理证明等技术有机结合起来，使之能自动验证软件安全性，并在不满足某性质时给出反例。研究利用所验证的公式获得最小谓词集；构造依赖所验证公式的最小近似抽象；在近似抽象模型中确定不合理反例，并使用OBDD布尔满足性问题求解最小谓词集，消除此不合理反例，精化抽象模型；根据抽象反例，通过路径仿真技术，确定具体反例路径。并且基于抽象解释的框架，及完备抽象解释和性质强保留之间的关系，构造公式的最小完备抽象。通过抽象解释理论及ASP(Answer set programming)，应用于安全协议验证、虚拟组织建模、装配序列生成和优化。本项目提出依赖所验证公式的弱性质保留抽象，以及最小完备抽象的方法，具有学术上的创新性，并且依赖公式抽象为软件程序抽象提供一种新的、有效的途径，为软件模型检测提供高效的支持。
结论摘要：
英文主题词Software verification; abstraction interpretation; predicate abstraction; model checking; complete abstraction
成果综合统计
期刊论文
会议论文
专利
获奖
著作
期刊论文
会议论文
相关项目
钱俊彦的项目
