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

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

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%.