结合可满足性模理论与抽象解释的程序分析技术研究

目录

第一个书签之前

摘 要

ABSTRACT

绪论

研究背景

现有技术和工具

基于抽象解释的程序分析

SMT在程序分析与验证中的应用

抽象解释与SMT的结合研究

研究内容

研究动机与目标

主要成果

论文结构

预备知识

程序的语法与语义

程序的语法

程序的语义

程序不变式

抽象解释基础

偏序集与格

Galois连接

不动点迭代

区间抽象域

区间抽象域的域表示

区间抽象域的域操作

可满足性模理论

SMT问题

SMT理论域

SMT库

SMT规划问题

小结

结合SMT的块级抽象解释

引言

块级抽象解释框架

基于分割点的块划分

基于SMT的程序块编码

复杂数据结构的SMT编码

SMT公式与抽象域表示的相互转化

结合SMT与抽象域的块级迭代

面向块级抽象解释框架的精度优化

基于谓词的块内状态划分

基于二叉决策树的抽象域提升算子

面向块级抽象解释框架的效率优化

基于稀疏性的大块切割

基于块级稀疏性的效率优化

实现与实验

小结

基于后向策略迭代的不动点求解方法

引言

基于策略迭代的程序不变式求解方法

局部策略迭代算法

后向策略迭代算法

路径选取阶段

路径验证阶段

算法描述及其复杂度分析

性质制导的后向策略迭代算法

面向性质验证的程序分析

算法的主要内容

算法的分析

实现与实验

小结

模版抽象域的设计与实现

引言

模版多面体抽象域

模版多面体抽象域的域表示

模版多面体抽象域的域操作

线性模版的生成策略

模版多面体抽象域的区间拓展

区间线性代数与区间线性规划

区间线性模版约束抽象域的域表示

区间线性模版约束抽象域的域操作

区间线性模版约束抽象域的模版生成策略

实现与实验

小结

结束语

工作总结

研究展望

致谢