基于计算机代数的程序验证
| 摘要 | 第1-4页 |
| ABSTRACT | 第4-10页 |
| 第一章 绪论 | 第10-18页 |
| ·研究背景 | 第10-12页 |
| ·研究现状 | 第12-16页 |
| ·主要工作及行文结构 | 第16-18页 |
| 第二章 不变量生成 | 第18-50页 |
| ·背景知识介绍 | 第18-27页 |
| ·循环归纳不变量和抽象解释 | 第18-24页 |
| ·Zone和Octagon抽象域 | 第24-25页 |
| ·演示抽象解释和Octagon抽象域 | 第25-27页 |
| ·改进Zone和Octagon抽象域 | 第27-50页 |
| ·抽象解释与归纳不变量 | 第28-30页 |
| ·基于量词消去的不变量生成 | 第30-50页 |
| ·对情形1的量词消去 | 第31-38页 |
| ·对情形2的量词消去 | 第38-41页 |
| ·对情形3的量词消去 | 第41-44页 |
| ·约束求解和生成尽可能强的不变量 | 第44-46页 |
| ·主算法的形式化描述及复杂度分析 | 第46-47页 |
| ·∞算术 | 第47-50页 |
| 第三章 不变量检测 | 第50-60页 |
| ·背景知识 | 第50-51页 |
| ·循环不变量的特征描述 | 第51-53页 |
| ·一种新的不变量―内循环不变量 | 第53-55页 |
| ·用内循环不变量调试程序 | 第55-58页 |
| ·生成非归纳不变量 | 第58-60页 |
| 第四章 带有线性约束的线性程序的终止性 | 第60-96页 |
| ·背景介绍 | 第60-64页 |
| ·半代数系统和工具包―DISCOVERER | 第64-65页 |
| ·一个基于符号计算的判定算法 | 第65-76页 |
| ·符号地计算(广义)特征向量 | 第65-68页 |
| ·主要算法 | 第68-74页 |
| ·例子 | 第74-76页 |
| ·正确性证明 | 第76-84页 |
| ·复杂性分析 | 第84-88页 |
| ·不可约情形 | 第88-96页 |
| ·一个充要条件 | 第89-91页 |
| ·算法 | 第91页 |
| ·例子 | 第91-93页 |
| ·复杂性分析 | 第93-96页 |
| 第五章 带有非线性约束的线性程序的终止性 | 第96-122页 |
| ·背景介绍 | 第96-98页 |
| ·LP_1、LQ_1、LR_1在Z上的不可判定性 | 第98-100页 |
| ·判定LP_1在R上的终止性算法 | 第100-109页 |
| ·A~nX的一般表达式 | 第100-102页 |
| ·n 次迭代之后P_j(X) 的一般表达式 | 第102-105页 |
| ·非零最小值性质 | 第105-108页 |
| ·主要算法 | 第108-109页 |
| ·正确性证明 | 第109-112页 |
| ·判定LQ_1 和LR_1 在R上的终止性算法 | 第112-114页 |
| ·相关的证明和子算法 | 第114-122页 |
| ·命题5.3的证明 | 第114-116页 |
| ·计算公共周期的算法 | 第116-118页 |
| ·求极大有理无关组的算法 | 第118-122页 |
| 第六章 结论和前景 | 第122-124页 |
| 参考文献 | 第124-130页 |
| 发表论文 | 第130-131页 |
| 致谢 | 第131-133页 |
