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

VSAR-CBMC: variable subgraph based multi-threaded program verification

作　　者：李运筹 尹平[1] 尹良泽[2] Li Yunchou;Yin Ping;Yin Liangze(Beijing Institution of Tracking ＆ Telecommunication Technology,Beijing 100094,China;School of Computers,National University of Defense Technology,Changsha 410073,China)

机构地区：[1]北京跟踪与通信技术研究所,北京100094 [2]国防科技大学计算机学院,长沙410073

出　　处：《计算机应用研究》2018年第8期2393-2396,共4页Application Research of Computers

摘　　要：Yogar-CBMC基于事件顺序图实现了反例抽象精化思想,是当前最有效的多线程程序验证工具之一。针对事件顺序图过于复杂,导致判断反例可行性及求解精化约束耗时过长的问题,提出变量子图概念及基于变量子图的抽象精化方法,将全局事件顺序图分解为连通等价的变量子图集,基于变量子图执行反例验证与精化求解,从而有效缩小图的规模,提升验证效率。将该方法实现为VSAR-CBMC,实验证明其相较于Yogar-CBMC验证时间平均缩短43%,有效提升了模型检验对并发程序的验证能力。Yogar-CBMC is among the most efficient multi-threaded program verification tools which implements counterexample guided abstract refinement based on event order graph（EOG）.However,due to the complexity of EOG,the counterexample validation and refinement constraints generation processes are usually time consuming,which significantly limits the scalability of Yogar-CBMC.This paper proposed a variable subgraph based abstract refinementmethod which decomposed the global EOG and shifted those EOG-relevant operations to the variable subgraph set.This paper implemented this method in Yogar-CBMC called VSAR-CBMC.Experimental results show that this method outperforms Yogar-CBMC by an average of 43%.

关 键 词：程序验证 变量子图 反例抽象精化 事件顺序图 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]