你好,游客 登录
背景:
阅读新闻

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

[日期:2017-06-29] 来源:计算机工程  作者:任胜兵,张健威,吴斌,王志健 [字体: ]

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

任胜兵,张健威,吴斌,王志健

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


temp_17062915448660.pdf

推荐 打印 | 录入: | 阅读:
相关新闻      
本文评论   
评论声明
  • 尊重网上道德,遵守中华人民共和国的各项有关法律法规
  • 承担一切因您的行为而直接或间接导致的民事或刑事法律责任
  • 本站管理人员有权保留或删除其管辖留言中的任意内容
  • 本站有权在网站内转载或引用您的评论
  • 参与本评论即表明您已经阅读并接受上述条款