《计算机应用研究》|Application Research of Computers

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

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

免费全文下载 (已被下载 次)  
获取PDF全文
作者 李运筹,尹平,尹良泽
机构 1.北京跟踪与通信技术研究所,北京 100094;2.国防科技大学 计算机学院,长沙 410073
统计 摘要被查看 次,已被下载
文章编号 1001-3695(2018)08-2393-04
DOI 10.3969/j.issn.1001-3695.2018.08.038
摘要 Yogar-CBMC基于事件顺序图实现了反例抽象精化思想,是当前最有效的多线程程序验证工具之一。针对事件顺序图过于复杂,导致判断反例可行性及求解精化约束耗时过长的问题,提出变量子图概念及基于变量子图的抽象精化方法,将全局事件顺序图分解为连通等价的变量子图集,基于变量子图执行反例验证与精化求解,从而有效缩小图的规模,提升验证效率。将该方法实现为VSAR-CBMC,实验证明其相较于Yogar-CBMC验证时间平均缩短43%,有效提升了模型检验对并发程序的验证能力。
关键词 程序验证;变量子图;反例抽象精化;事件顺序图
基金项目
本文URL http://www.arocmag.com/article/01-2018-08-038.html
英文标题 VSAR-CBMC: variable subgraph based multi-threaded program verification
作者英文名 Li Yunchou, Yin Ping, Yin Liangze
机构英文名 1.BeijingInstitutionofTracking&TelecommunicationTechnology,Beijing100094,China;2.SchoolofComputers,NationalUniversityofDefenseTechnology,Changsha410073,China
英文摘要 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%.
英文关键词 program verification; variable subgraph; CEGAR; event order graph
参考文献 查看稿件参考文献
  [1] Kroening D. Automated verification of concurrent software[C] //Reachability Problems. Berlin:Springer, 2013:19-20.
[2] Biere A, Cimatti A, Clarke E M, et al. Bounded model checking[C] //Advances in Computers. Salt Lake City:Academic Press, 2003:117-148.
[3] Clarke E M, Kroening D, Lerda F. A tool for checking ANSI-C programs[C] //Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer-Verlag, 2004:168-176.
[4] Lucas C, Fischer B. Verifying multi-threaded software using SMT-based context-bounded model checking[C] //Proc of the 33rd International Conference on Software Engineering. New York:ACM Press, 2011:331-340. [5] Cadar C, Ganesh V, Pawlowski P M, et al. EXE:automatically generating inputs of death[J] . ACM Trans on Information and System Security, 2008, 12(2):1-38.
[6] Ivancˇic′ F, Yang Z, Ganai M K, et al. F-SOFT:software verification platform[C] //Proc of International Conference on Computer Aided Verification. Berlin:Springer, 2005:301-306.
[7] Xie Yichen, Alexander A. Saturn:a SAT-based tool for bug detection[C] //Proc of International Conference on Computer Aided Verification. Berlin:Springer, 2005:139-143.
[8] Monteiro F R, Alves E H S, Silva I S, et al. ESBMC-GPU:a context-bounded model checking tool to verify CUDA programs[J] . Science of Computer Programming, 2018, 152(1):63-69.
[9] Fischer B, Inverso O, Parlato G. CSeq:a sequentialization tool for C[C] //Tools and Algorithms for the Construction and Analysis of Systems. Berlin :Springer, 2013:616-618.
[10] Inverso O, Tomasco E, Fischer B, et al. Bounded model checking of multi-threaded C programs via lazy sequentialization[C] //Computer Aided Verification. Cham:Springer, 2014:585-602.
[11] Tomasco E, Inverso O, Fischer B, et al. Verifying concurrent programs by memory unwinding[C] //Tools and Algorithms for Construction and Analysis of Systems. Berlin:Springer, 2015:551-565.
[12] Ishai R, Grumberg O. Bounded model checking of concurrent programs[C] //Proc of International Conference on Computer Aided Verification. Berling:Springer, 2005:319-325.
[13] Qadeer S, Rehof J. Context-bounded model checking of concurrent software[C] //Tools and Algorithms for the Construction and Analysis of System. Berlin:Springer-Verlag, 2005:93-107.
[14] Cook B, Kroening D, Sharygina N. Symbolic model checking for asynchronous Boolean programs[C] //Model Checking and Software Verification. Berlin:Springer-Verlag, 2005:75-90.
[15] Alglave J, Kroening D, Tautschnig M. Partial orders for efficient bounded model checking of concurrent software[C] //Computer Aided Verification. Berlin:Springer, 2013:141-157.
[16] Yin Liangze, Dong Wei, Liu Wanwei, et al. Scheduling constraint based abstraction refinement for multi-threaded program verification[EB/OL] . (2016-01)[2017-11-14] . https://arxiv. org/abs/1708. 08323.
收稿日期 2017/9/13
修回日期 2017/11/15
页码 2393-2396
中图分类号 TP311.5
文献标志码 A