基于可满足性模理论求解器的程序路径验证方法

针对程序中因存在路径条数过多或复杂循环路径而导致路径验证时的路径搜索空间过大,直接影响验证的效率和准确率的问题,提出一种基于可满足性模理论(SMT)求解器的程序路径验证方法。首先利用决策树的方法对复杂循环路径提取不变式,构造无循环控制流图(NLCFG);然后通过基本路径法对控制流图(CFG)进行遍历,提取基本路径信息;最后利用SMT求解器作为约束求解器,将路径验证问题转化为约束求解问题来进行处理。与同样基于SMT求解器的路径验证工具CBMC和FSoft-SMT相比,该方法在对测试集程序的验证时间上比CBMC降低了25%以上,比FSoft-SMT降低了15%以上;在验证精度上,该方法有明显的提升。实验结果表明,方法可以有效解决路径搜索空间过大的问题,同时提高路径验证的效率和准确率。

可满足模理论在软硬件划分领域的应用

软硬件划分是评价软硬件协同设计优劣,甚至影响设计成败的关键技术之一.文章首次将可满足模理论应用于软硬件划分问题,借助Z3、CVC4与MathSAT5可满足问题解决器求得最优的软硬件划分方案,使得系统的软硬件实现代价最小,经实验验证,针对软硬件划分问题,Z3的综合性能要优于另外两种解决器.采用可满足性问题求解方案,不仅克服了传统启发式算法陷入局部最优解的弊端,同时也弥补了规划类算法不适应于大规模划分问题的不足.

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

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