Concurrent Bounded Model Checking
ACM SIGSOFT Software Engineering Notes(2015)
摘要
We introduce a methodology, based on symbolic execution, for Concurrent Bounded Model Checking. In our approach, we translate a program into a formula in a disjunctive form. This design enables concurrent verification, with a main thread running symbolic execution, without any constraint solving, to build subformulas, and a set of worker threads running a decision procedure for satisfiability checks. We have implemented this methodology in a tool called JCBMC, the first bounded model checker for Java. JCBMC is built as an extension of Java Pathfinder, an open-source verification platform developed by NASA. JCBMC uses Symbolic PathFinder (SPF) for the symbolic execution, Z3 as the solver and implements concurrency with multi-threading. For evaluation, we compare JCBMC against SPF and the Bounded Model Checker CBMC. The results of the experiments show that we can achieve significant advantages of performance over these two tools.
更多查看译文
关键词
algorithms,symbolic execution,concurrent programming,verification,software/program verification,concurrency,theory,bounded model checking,performance
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要