基于抽象-验证-细化范例的软件模型检测

• 作者: 刘吉锋 孙吉贵
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 模型检测 软件模型检测 谓词抽象 反例驱动的细化
• 年，卷（期）: 2006,（12）
• 所属期刊栏目: 软件工程
• 页码范围: 255-260
• 页数: 6页
• 分类号: TP3
• 字数: 10025字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2006.12.067

摘要

如何保证软件系统的正确性和可靠性是当前软件开发面临的主要问题之一.模型检测作为一种重要的自动化验证技术在软件的分析与验证中正取得越来越多的成功.本文以微软的SLAM和加州大学伯克利分校的BLAST为例综述性地介绍了基于抽象-验证-细化范例的软件模型检测.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	孙吉贵	吉林大学符号计算与知识工程教育部重点实验室	134	2984	21.0	52.0
2	刘吉锋	吉林大学计算机科学与技术学院	2	14	2.0	2.0