| 摘要 | 第1-9页 |
| ABSTRACT | 第9-10页 |
| 第一章 绪论 | 第10-18页 |
| ·课题研究背景 | 第10-15页 |
| ·形式化验证方法 | 第10-11页 |
| ·验证工具 | 第11-15页 |
| ·问题描述 | 第15页 |
| ·课题研究思路与内容 | 第15-16页 |
| ·课题创新点 | 第16-17页 |
| ·论文结构 | 第17-18页 |
| 第二章 SMT 求解技术及 ω-自动机理论 | 第18-27页 |
| ·SMT 求解技术相关概念及理论 | 第18-22页 |
| ·可满足性问题(SAT) | 第18-20页 |
| ·可满足性模理论问题(SMT) | 第20-22页 |
| ·ω-自动机理论相关概念及理论 | 第22-27页 |
| ·ω-自动机 | 第22-25页 |
| ·ω-自动机语言识别及其判空问题 | 第25-27页 |
| 第三章 基于当前工业应用的 SMT 求解器技术分析以及能力对比实验 | 第27-40页 |
| ·SMT 求解器理论组合判定技术对比分析 | 第27-33页 |
| ·Nelson-Oppen 方法 | 第28-30页 |
| ·Delayed Theory Combination 方法 | 第30-31页 |
| ·Ackerman 化方法 | 第31-32页 |
| ·主流 SMT 求解器理论组合判定技术对比 | 第32-33页 |
| ·SMT 求解器理论组合判定技术对比实验 | 第33-38页 |
| ·SMT-COMP 中 SMT 求解器理论组合判定技术对比 | 第33-34页 |
| ·面向工业应用的 SMT 求解器理论组合判定技术对比实验 | 第34-38页 |
| ·本章小结 | 第38-40页 |
| 第四章 基于 ω-自动机判空的 SMT 求解器能力扩展 | 第40-48页 |
| ·SMT 求解器量词推理技术的局限性 | 第40-41页 |
| ·一类 SMT 求解器目前无法判定的量化 SMT 公式一般形式 | 第41-42页 |
| ·迁移系统/自动机的符号化表示 | 第42-45页 |
| ·量化 SMT 公式转化为自动机的符号化表示 | 第45-47页 |
| ·本章小结 | 第47-48页 |
| 第五章 基于自动机判空的 SMT 求解器能力扩充的实现 | 第48-59页 |
| ·输入文件语法分析 | 第48-49页 |
| ·自动机符号化表示语法分析 | 第49-51页 |
| ·实验框架设计 | 第51-52页 |
| ·实现部分 | 第52-58页 |
| ·实验环境配置 | 第52页 |
| ·例 1 的实验结果 | 第52-55页 |
| ·例 2 的实验结果 | 第55-58页 |
| ·本章小结 | 第58-59页 |
| 第六章 结束语 | 第59-60页 |
| ·本文工作总结 | 第59页 |
| ·下一步工作 | 第59-60页 |
| 致谢 | 第60-61页 |
| 参考文献 | 第61-65页 |
| 作者在学期间取得的学术成果 | 第65-66页 |
| 附录 A SMT 理论域 | 第66页 |
