摘  要

        抽象解释理论是Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近程序的不动点理论。它的一个重要应用是分析程序中的变量或约束表达式的值域。这些值域信息有助于进行数组和循环的界限分析，基于数组的数据依赖性分析，指针分析，循环时间分析，可执行路径分析等。

        抽象解释理论的特点是可靠但不完备的，即：如果验证结果表明抽象系统满足验证性质，则抽象解释理论保证原系统也满足验证性质；若验证结果表明抽象系统不满足验证性质，则原系统可能满足验证性质，可能不满足验证性质，需要更精细的抽象分析。而一个精确的抽象域能够减少这种不完备性，有利于提高验证效率。因此，设计一个精确的抽象域及定义抽象域上抽象运算是抽象解释理论研究的核心内容。

        本文利用抽象解释理论对浮点数表达式约束问题的值域进行了估测，主要的目标改善不完备性。其主要工作如下：

        首先，基于IEEE 754-1985浮点数模型规范，结合抽象解释理论中的完备格的性质，本文提出了浮点数的抽象语义。然后根据区间抽象域的一些运算特性和IEEE 754-1985浮点数模型的舍入模式，定义了这种抽象域的抽象运算。

        其次，为均衡浮点数表达式的计算精度和计算效率，在浮点数抽象模型以及抽象运算的基础上，本文为两个变量的浮点数线性表达式约束问题建立区间约束。为区间约束建立区间约束图，在约束图的基础上，把这类浮点数约束问题转化为区间线性方程。利用上面定义的区间运算，本文给出了这类问题的解。

        最后，本文提出的的算法与以往的利用加宽算子或者是收缩算子方法进行比较，发现本文算法所找到的抽象域能够更准确更有效地反映可达状态集，可以简化在这个抽象域上的抽象运算，大大地减少虚假的错误报告。

关键词：程序静态分析；抽象解释理论；区间抽象域；浮点数表达式约束问题；加宽算子或者是收缩算子

论文报告