|
|
|
|
基于CEGAR的C程序模型检测研究 |
| |
| 论文目录 |
| |
| 摘要 | 第5-7页 | | ABSTRACT | 第7-8页 | | 符号对照表 | 第13-16页 | | 缩略语对照表 | 第16-21页 | | 第一章 绪论 | 第21-31页 | | 1.1 研究背景和意义 | 第21-22页 | | 1.2 研究现状 | 第22-28页 | | 1.2.1 模型检测的研究概况 | 第23-26页 | | 1.2.2 基于CEGAR的模型检测技术研究现状 | 第26-27页 | | 1.2.3 程序验证中处理循环的研究 | 第27-28页 | | 1.3 研究内容 | 第28-30页 | | 1.4 论文组织结构 | 第30-31页 | | 第二章 研究的技术背景 | 第31-39页 | | 2.1 基础概念 | 第31-34页 | | 2.2 基于CEGAR的抽象模型检测 | 第34-38页 | | 2.3 本章小结 | 第38-39页 | | 第三章 采用插值的CEGAR模型检测方法 | 第39-73页 | | 3.1 研究背景和动机 | 第39-42页 | | 3.2 新的Craig插值应用 | 第42-56页 | | 3.2.1 安全插值 | 第42-49页 | | 3.2.2 错误插值 | 第49-55页 | | 3.2.3 改进后的算法框架 | 第55-56页 | | 3.3 优化策略 | 第56-64页 | | 3.3.1 裁剪控制流图 | 第59-61页 | | 3.3.2 基于权重的搜索策略 | 第61-64页 | | 3.4 实验与分析 | 第64-70页 | | 3.4.1 实验设计 | 第64-66页 | | 3.4.2 插值的有效性分析 | 第66-69页 | | 3.4.3 错误插值的正确性分析 | 第69-70页 | | 3.5 本章小结 | 第70-73页 | | 第四章 基于懒惰抽象的C程序时序性质验证 | 第73-105页 | | 4.1 引言 | 第73-75页 | | 4.2 传统的时序性质验证方法 | 第75-81页 | | 4.2.1 安全性质的验证 | 第75-77页 | | 4.2.2 时序性质的验证 | 第77-80页 | | 4.2.3 面临的挑战性问题 | 第80-81页 | | 4.3 基于CEGAR的C程序空指针解引用检测方法 | 第81-92页 | | 4.3.1 无穷模型上的线性时序逻辑 | 第81-85页 | | 4.3.2 空指针解引用的LTL描述 | 第85-87页 | | 4.3.3 采用CEGAR技术验证空指针解引用问题 | 第87-92页 | | 4.4 有穷模型上的时序性质验证方法 | 第92-98页 | | 4.4.1 有穷模型上的线性时序逻辑 | 第92-96页 | | 4.4.2 采用on-the-fly技术产生反例路径 | 第96-97页 | | 4.4.3 基于CEGAR的有穷模型验证 | 第97-98页 | | 4.5 实现与实验 | 第98-103页 | | 4.5.1 空指针解引用问题的算法评估 | 第99-100页 | | 4.5.2 有穷模型上时序性质验证的算法评估 | 第100-103页 | | 4.6 本章小结 | 第103-105页 | | 第五章 反例检测加速算法研究 | 第105-125页 | | 5.1 研究背景和动机 | 第105-108页 | | 5.2 一个详细的验证示例 | 第108-110页 | | 5.3 循环分类和处理方法 | 第110-118页 | | 5.3.1 简单循环和复杂循环 | 第110-112页 | | 5.3.2 一种有效处理简单循环的方法 | 第112-118页 | | 5.3.3 采用动态执行处理复杂循环的方法 | 第118页 | | 5.4 算法实现和实验 | 第118-123页 | | 5.4.1 循环分类 | 第119-123页 | | 5.5 本章小节 | 第123-125页 | | 第六章 总结与展望 | 第125-129页 | | 6.1 工作总结 | 第125-126页 | | 6.2 工作展望 | 第126-129页 | | 参考文献 | 第129-141页 | | 致谢 | 第141-143页 | | 作者简介 | 第143-145页 |
|
|
|
|
论文编号BS4415444，这篇论文共145页
会员购买按0.35元/页下载，共需支付50.75元。 直接购买按0.5元/页下载，共需要支付72.5元 。 |
 |
 |
我还不是会员，注册会员！
会员下载更优惠!充值送钱！ |
我只需要这篇，无需注册！
直接网上支付，方便快捷！ |
|
|
|
版权申明：本目录由www.jylw.com网站制作，本站并未收录原文，如果您是作者，需要删除本篇论文目录请通过QQ或其它联系方式告知我们，我们承诺24小时内删除。 |
|
|
广告服务