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

• 作者: 任胜兵 吴斌 张健威 王志健
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 软件验证 限界模型检测 弹性分布式数据集 可满足性模理论求解器 Spark框架
• 年，卷（期）: 2017,（6）
• 所属期刊栏目: 体系结构与软件技术
• 页码范围: 19-23,29
• 页数: 6页
• 分类号: TP311
• 字数: 3938字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2017.06.003

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	任胜兵	中南大学软件学院嵌入式系统与网络实验室	46	292	8.0	16.0
2	吴斌	中南大学软件学院嵌入式系统与网络实验室	49	383	10.0	18.0
3	张健威	中南大学软件学院嵌入式系统与网络实验室	2	2	1.0	1.0
4	王志健	中南大学软件学院嵌入式系统与网络实验室	3	5	2.0	2.0