-
题名VASR-CBMC:基于变量子图的多线程程序验证
- 1
-
-
作者
李运筹
尹平
尹良泽
-
机构
北京跟踪与通信技术研究所
国防科技大学计算机学院
-
出处
《计算机应用研究》
CSCD
北大核心
2018年第8期2393-2396,共4页
-
文摘
Yogar-CBMC基于事件顺序图实现了反例抽象精化思想,是当前最有效的多线程程序验证工具之一。针对事件顺序图过于复杂,导致判断反例可行性及求解精化约束耗时过长的问题,提出变量子图概念及基于变量子图的抽象精化方法,将全局事件顺序图分解为连通等价的变量子图集,基于变量子图执行反例验证与精化求解,从而有效缩小图的规模,提升验证效率。将该方法实现为VSAR-CBMC,实验证明其相较于Yogar-CBMC验证时间平均缩短43%,有效提升了模型检验对并发程序的验证能力。
-
关键词
程序验证
变量子图
反例抽象精化
事件顺序图
-
Keywords
program verification
variable subgraph
CEGAR
event order graph
-
分类号
TP311.5
[自动化与计算机技术—计算机软件与理论]
-