基于区间线性抽象域的可靠浮点及非凸静态分析
| 摘要 | 第1-13页 |
| ABSTRACT | 第13-15页 |
| 第一章 绪论 | 第15-37页 |
| ·研究背景 | 第15-21页 |
| ·程序的数值性质 | 第17-18页 |
| ·数值抽象解释及其应用 | 第18-21页 |
| ·研究目标及主要结果 | 第21-29页 |
| ·研究动机 | 第21-26页 |
| ·研究目标 | 第26-27页 |
| ·主要结果 | 第27-29页 |
| ·相关研究工作 | 第29-34页 |
| ·数值抽象域 | 第29-31页 |
| ·非凸静态分析 | 第31-32页 |
| ·浮点计算的分析与验证 | 第32-33页 |
| ·区间线性代数 | 第33-34页 |
| ·论文结构 | 第34-37页 |
| 第二章 基于抽象解释的数值程序分析 | 第37-71页 |
| ·引言 | 第37页 |
| ·预备知识 | 第37-40页 |
| ·偏序、格 | 第37-38页 |
| ·不动点 | 第38-40页 |
| ·抽象解释理论 | 第40-49页 |
| ·基于Galois连接的抽象解释 | 第40-42页 |
| ·基于具体化函数的抽象解释 | 第42页 |
| ·抽象不动点 | 第42-47页 |
| ·迭代策略 | 第47-48页 |
| ·抽象域 | 第48-49页 |
| ·数值程序分析与数值抽象域 | 第49-57页 |
| ·数值程序的建模与分析 | 第49-51页 |
| ·数值抽象域的设计 | 第51-54页 |
| ·有数值抽象域概览 | 第54-57页 |
| ·面向浮点程序的静态分析与基于浮点的抽象域实现 | 第57-69页 |
| ·IEEE 754浮点模型 | 第58-60页 |
| ·面向浮点程序的分析 | 第60-68页 |
| ·基于浮点的抽象域实现 | 第68-69页 |
| ·小结 | 第69-71页 |
| 第三章 浮点多面体抽象域 | 第71-103页 |
| ·引言 | 第71-72页 |
| ·基于约束的有理数多面体域 | 第72-79页 |
| ·域表示 | 第72页 |
| ·域操作 | 第72-79页 |
| ·基于约束的浮点多面体域 | 第79-89页 |
| ·域表示 | 第79页 |
| ·浮点Fourier-Motzkin消除法 | 第79-82页 |
| ·严格线性规划 | 第82-84页 |
| ·浮点多面体域的可靠性 | 第84-85页 |
| ·精度和效率改进策略 | 第85-89页 |
| ·基于约束的多面体域的弱接合 | 第89-95页 |
| ·基于模版的弱接合 | 第90-91页 |
| ·基于包络和界信息的弱接合 | 第91-92页 |
| ·基于两变量约束的弱接合 | 第92-94页 |
| ·启发式结合策略 | 第94-95页 |
| ·实现及实验 | 第95-100页 |
| ·小结 | 第100-103页 |
| 第四章 区间多面体抽象域 | 第103-127页 |
| ·引言 | 第103-104页 |
| ·区间线性代数 | 第104-106页 |
| ·区间线性不等式系统 | 第105-106页 |
| ·区间线性规划 | 第106页 |
| ·区间多面体域 | 第106-118页 |
| ·域表示 | 第106-109页 |
| ·域操作 | 第109-116页 |
| ·应用 | 第116-118页 |
| ·单变量区间线性不等式域 | 第118-122页 |
| ·实现及实验 | 第122-124页 |
| ·小结 | 第124-127页 |
| 第五章 行阶梯形区间线性等式抽象域 | 第127-151页 |
| ·引言 | 第127-128页 |
| ·带无穷区间系数的区间线性等式系统 | 第128-130页 |
| ·行阶梯形区间线性等式域 | 第130-142页 |
| ·域表示 | 第130-132页 |
| ·域操作 | 第132-142页 |
| ·实现及实验 | 第142-150页 |
| ·实现 | 第142-143页 |
| ·INTERPROC实验 | 第143-145页 |
| ·ASTRIDE实验 | 第145-150页 |
| ·小结 | 第150-151页 |
| 第六章 面向线性绝对值及广义线性互补关系的抽象域 | 第151-183页 |
| ·引言 | 第151-153页 |
| ·线性绝对值系统及其等价刻画 | 第153-158页 |
| ·线性绝对值不等式系统及其等价刻画 | 第156-158页 |
| ·线性绝对值等式系统及其等价刻画 | 第158页 |
| ·广义线性互补问题的双重描述法 | 第158-167页 |
| ·从约束表示到生成子表示的转化 | 第159-165页 |
| ·从生成子表示到约束表示的转化 | 第165-166页 |
| ·应用：绝对值线性规划 | 第166-167页 |
| ·线性绝对值不等式域 | 第167-173页 |
| ·域表示 | 第167页 |
| ·域操作 | 第167-173页 |
| ·线性绝对值等式域 | 第173-177页 |
| ·域表示 | 第173-174页 |
| ·域操作 | 第174-177页 |
| ·实现及实验 | 第177-180页 |
| 6 7 小结 | 第180-183页 |
| 第七章 结束语 | 第183-187页 |
| 7 1 工作总结 | 第183-184页 |
| ·研究展望 | 第184-187页 |
| 致谢 | 第187-189页 |
| 参考文献 | 第189-203页 |
| 作者在学期间取得的学术成果 | 第203页 |
