资料下载
×
基于SMT求解器的程序路径验证方法
消耗积分:1 |
格式:rar |
大小:0.78 MB |
2017-12-11
分享资料个
针对程序中因存在路径条数过多或复杂循环路径而导致路径验证时的路径搜索空间过大，直接影响验证的效率和准确率的问题，提出一种基于可满足性模理论（SMT）求解器的程序路径验证方法。首先利用决策树的方法对复杂循环路径提取不变式，构造无循环控制流图（ NLCFG）；然后通过基本路径法对控制流图（CFG）进行遍历，提取基本路径信息；最后利用SMT求解器作为约束求解器，将路径验证问题转化为约束求解问题来进行处理。与同样基于SMT求解器的路径验证工具CBMC和FSoft-SMT相比，该方法在对测试集程序的验证时间上比CBMC降低了25%以上，比FSoft-SMT降低了15%以上；在验证精度上，该方法有明显的提升。实验结果表明，方法可以有效解决路径搜索空间过大的问题，同时提高路径验证的效率和准确率。
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
