谓词抽象技术研究

• 作者: 屈婉霞 李暾 杨晓东 郭阳
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 模型检验 谓词抽象 抽象求精 反例 插值
• 年，卷（期）: 2008,（1）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 27-38
• 页数: 12页
• 分类号: TP301
• 字数: 12197字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2008.00027

摘要

随着软、硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.谓词抽象是解决状态空间爆炸的最有效方法之一,近年来得到迅速发展.介绍了谓词抽象的基本算法并比较了不同的求解支持工具;重点分析了反例指导的抽象求精和基于插值的抽象求精原理;分析了产生新谓词的各种方法的优、缺点;最后指出了谓词抽象技术进一步发展所面临的挑战和发展方向.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭阳	国防科学技术大学计算机学院	39	252	9.0	14.0
2	李暾	国防科学技术大学计算机学院	29	182	7.0	12.0
3	杨晓东	国防科学技术大学计算机学院	18	186	7.0	13.0
4	屈婉霞	国防科学技术大学计算机学院	8	88	5.0	8.0