论文部分内容阅读
在基于可满足性模理论（SMT）的限界模型检测中，限界深度对于程序验证结果的可信性和程序验证效率具有重要影响。传统串行检测方法由于单机处理性能和内存的限制，不能在限界较深的条件下进行验证。针对该问题，在Spark环境下提出一种分布式限界模型检测方法。将源程序的LLVM中间表示（LLVM-IR）构造为Spark内置的数据结构PairRDD，利用MapReduce算法将PairRDD转化为表示验证条件的弹性分布式数据集（VCsRDD），VCsRDD转化为SMT-LIB并输入SMT求解器进行验证。实验结果表明，与