堆操作程序分析验证技术研究
| 摘要 | 第1-12页 |
| Abstract | 第12-14页 |
| 第一章 绪论 | 第14-26页 |
| ·堆操作程序相关的可信性质 | 第14-16页 |
| ·相关研究工作 | 第16-22页 |
| ·通用形式化分析验证技术 | 第16-18页 |
| ·堆操作程序分析验证技术 | 第18-20页 |
| ·堆内存抽象模型 | 第20-22页 |
| ·本文的主要研究内容 | 第22-25页 |
| ·论文结构 | 第25-26页 |
| 第二章 单向链表抽象模型 | 第26-54页 |
| ·链表操作语法 | 第27-28页 |
| ·单向无环链表的抽象模型 | 第28-39页 |
| ·基本模型定义 | 第28-33页 |
| ·链表操作抽象语义 | 第33-39页 |
| ·环形链表扩展 | 第39-48页 |
| ·基本模型定义 | 第39-43页 |
| ·链表操作抽象语义 | 第43-48页 |
| ·实验 | 第48-51页 |
| ·本章小结 | 第51-54页 |
| 第三章 双向链表抽象模型 | 第54-76页 |
| ·FreeRTOS 中的双向链表 | 第54-55页 |
| ·基本模型定义 | 第55-63页 |
| ·链表操作抽象语义 | 第63-69页 |
| ·实验 | 第69-70页 |
| ·链表抽象模型小结 | 第70-74页 |
| ·链表抽象模型相关工作及对比 | 第70-72页 |
| ·文中链表抽象模型的特点 | 第72-74页 |
| ·本章小结 | 第74-76页 |
| 第四章 堆操作程序符号化数值抽象框架 | 第76-92页 |
| ·研究动机及主要思想 | 第76-78页 |
| ·抽象状态迁移图 | 第78-80页 |
| ·符号化数量形态分析 | 第80-86页 |
| ·抽象状态间的subsumption 关系 | 第81-82页 |
| ·构造抽象状态迁移图 | 第82-86页 |
| ·面向性质的数值模型抽象 | 第86-89页 |
| ·实验结果 | 第89-90页 |
| ·本章小结 | 第90-92页 |
| 第五章 面向链表的形态数量抽象域 | 第92-112页 |
| ·研究动机及主要思想 | 第92-94页 |
| ·域表示 | 第94-95页 |
| ·域操作 | 第95-100页 |
| ·迁移函数 | 第100-107页 |
| ·条件测试语句的迁移函数 | 第100-102页 |
| ·链表操作语句的迁移函数 | 第102-107页 |
| ·案例应用分析 | 第107-109页 |
| ·本章小结 | 第109-112页 |
| 第六章 堆内存上界分析 | 第112-126页 |
| ·堆内存使用量建模 | 第112-113页 |
| ·链表操作程序堆内存上界分析 | 第113-115页 |
| ·基于符号执行的堆内存上界分析 | 第115-123页 |
| ·堆内存建模 | 第116-117页 |
| ·循环处理策略 | 第117-121页 |
| ·实验结果 | 第121-123页 |
| ·相关工作及对比 | 第123-124页 |
| ·本章小结 | 第124-126页 |
| 第七章 结论与展望 | 第126-130页 |
| ·本文的主要贡献 | 第126-127页 |
| ·下一步研究工作 | 第127-130页 |
| 致谢 | 第130-132页 |
| 参考文献 | 第132-140页 |
| 作者在学期间取得的学术成果 | 第140-142页 |
| 附录 A 相关定理证明 | 第142-146页 |
