VASR-CBMC:基于变量子图的多线程程序验证

• 作者: 尹平 尹良泽 李运筹
• 来源期刊: 计算机应用研究
• 关键词: 程序验证 变量子图 反例抽象精化 事件顺序图
• 年，卷（期）: 2018,（8）
• 所属期刊栏目: 软件技术研究
• 页码范围: 2393-2396
• 页数: 4页
• 分类号: TP311.5
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2018.08.038

摘要

Yogar-CBMC基于事件顺序图实现了反例抽象精化思想,是当前最有效的多线程程序验证工具之一.针对事件顺序图过于复杂,导致判断反例可行性及求解精化约束耗时过长的问题,提出变量子图概念及基于变量子图的抽象精化方法,将全局事件顺序图分解为连通等价的变量子图集,基于变量子图执行反例验证与精化求解,从而有效缩小图的规模,提升验证效率.将该方法实现为VSAR-CBMC,实验证明其相较于Yogar-CBMC验证时间平均缩短43％,有效提升了模型检验对并发程序的验证能力.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	尹平		9	192	4.0	9.0
2	李运筹		2	2	1.0	1.0
3	尹良泽	国防科技大学计算机学院	7	22	3.0	4.0