采用CPAChecker的动态程序验证

• 作者: 刘锟龙 段钊
• 来源期刊: 西安电子科技大学学报（自然科学版）
• 学科: 工学
• 关键词: 模型检测 抽象精化 动态执行 程序验证 状态空间爆炸
• 年，卷（期）: 2019,（1）
• 页码范围: 33-38
• 页数: 6页
• 分类号: TP302.7
• 字数: 5121字
• 语种: 中文
• DOI: 10.19665/j.issn1001-2400.2019.01.06

摘要

针对模型检测中状态空间爆炸问题,在CPAChecker的抽象谓词检测方法的基础上,提出了一种基于动态执行的检测方法.首先,根据程序的控制流程图,对程序进行静态检测.在静态检测的过程中,根据分支语句的确定性,利用动态执行的方法来加快检测的过程.其中,抽象检测可以有效地限制系统模型的规模,动态执行不仅可以有效地减少静态检测导致的误判,而且有助于引导构建精确的系统模型,降低虚假反例的数量和不必要的反例分析和精化.实验数据显示,这种算法明显提高了传统的反例引导谓词抽象精化算法的检测效率和准确率.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘锟龙	合肥工业大学电气与自动化工程学院	2	3	1.0	1.0
2	段钊	西安电子科技大学计算机学院	2	10	2.0	2.0