资料下载
×
一种分布式限界模型检测方法
消耗积分:1 |
格式:rar |
大小:1.73 MB |
2018-02-02
分享资料个
在基于可满足性模理论（SMT）的限界模型检测中，限界深度对于程序验证结果的可信性和程序验证效率具有重要影响。传统串行检测方法由于单机处理性能和内存的限制，不能在限界较深的条件下进行验证。针对该问题，在Spark环境下提出一种分布式限界模型检测方法。将源程序的LLVM中间表示（LLVM-IR）构造为Spark内置的数据结构Pair RDD，利用MapReduce算法将Pair RDD转化为表示验证条件的弹性分布式数据集（VCs RDD），VCs RDD转化为SMT-LIB并输入SMT求解器进行验证。实验结果表明，与传统串行检测方法相比，该方法提高了验证过程中的限界深度和验证结果的正确率，并且对于复杂度较高的程序在限界相同的情况下其验证速度也有所提升。
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
