基于程序局部性引导的有界模型检测优化方法

• 作者: 刘吉强 杜晔 王舜 韩臻
• 来源期刊: 通信学报
• 学科: 工学
• 关键词: 模型检测 BMC 软件检测 局部性 优化
• 年，卷（期）: 2018,（3）
• 所属期刊栏目: 论文Ⅱ:学术论文
• 页码范围: 181-190
• 页数: 10页
• 分类号: TP311.1
• 字数: 10263字
• 语种: 中文
• DOI: 10.11959/j.issn.1000-436x.2018050

摘要

基于多种模型检测方法组合的复合检测方式是当前软件模型检测领域开展研究的热点之一.在当前的研究中,提高检测的规模和检测的对象复杂程度的关键在于如何有效处理抽象的扩张和收缩.证明通过对程序模式或验证信息的利用可以加快状态空间的探索速度.面向有界模型检测(BMC)加速方法展开研究,使用程序中额外的信息和知识对其处理以协助检测器删除冗余和无效的状态.在对程序局部性进行定义的基础上,对其加速性进行讨论,提出一种加速有界检测的方法和一种改进策略,对算法进行了详细描述,并通过实验验证了方法在检测效率和性能上的优越性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	韩臻	北京交通大学智能交通数据安全与隐私保护技术北京市重点实验室	108	966	17.0	26.0
2	刘吉强	北京交通大学智能交通数据安全与隐私保护技术北京市重点实验室	66	535	13.0	21.0
3	杜晔	北京交通大学智能交通数据安全与隐私保护技术北京市重点实验室	20	75	6.0	8.0
4	王舜	北京交通大学智能交通数据安全与隐私保护技术北京市重点实验室	2	1	1.0	1.0