Spark环境下基于SMT的分布式限界模型检测

SMT-based Distributed Bounded Model Checking in Spark

在基于可满足性模理论(SMT)的限界模型检测中,限界深度对于程序验证结果的可信性和程序验证效率具有重要影响。传统串行检测方法由于单机处理性能和内存的限制,不能在限界较深的条件下进行验证。针对该问题,在Spark环境下提出一种分布式限界模型检测方法。将源程序的LLVM中间表示(LLVM-IR)构造为Spark内置的数据结构Pair RDD,利用MapReduce算法将Pair RDD转化为表示验证条件的弹性分布式数据集(VCs RDD),VCs RDD转化为SMT-LIB并输入SMT求解器进行验证。实验结果表明,与传统串行检测方法相比,该方法提高了验证过程中的限界深度和验证结果的正确率,并且对于复杂度较高的程序在限界相同的情况下其验证速度也有所提升。

The credibility of program verification results and the verification efficiency in Satisfiablity Modulo Theories （SMT） -based bounded model checking are influenced greatly by bounds. However, the traditional serial checking method cannot validate under the conditions of too large bounds because of the limitation of handling performance and memory in a single machine. In order to solve this problem, this paper proposes a SMT-based distributed BMC method in Spark. First of all,the LLVM Intermediate Representation （LLVM-IR） translated from the source program is converted into Spark built-in data structure Pair Resilient Distributed Dataset（RDD）. Afterwards, the Pair RDD is converted into Verification Conditions RDD （VCs RDD） which is then converted into SMT-LIB with the proposed MapReduce algorithm. In the end,the proposed method utilizes SMT solver for verification with the SMT-LIB. Experimental results indicate that, compared with the traditional serial checking method, the proposed method improves not only the bounds of the validation process and the correctness of the verification results, but also the speed of verification for the program with higher comolexity under the same bound.