基于浮点区间幂集抽象域的浮点程序分析

摘要：

浮点变量在程序中的取值范围对浮点程序中相关性质的分析及运行时错误的检查具有重要意义.浮点运算的不精确性使得浮点变量的值范围分析具有挑战性.抽象解释理论为程序变量的值范围分析提供了一个通用的框架.在抽象解释的框架下,提出了一个新的数值抽象域——区间幂集抽象域,即使用有限个区间的析取来刻画变量的取值范围.该抽象域的表达能力强于经典的区间抽象域,能够较好地刻画大部分已有抽象域不能表达的非凸性质,从而有效提高分析精度.在此基础上,给出了区间幂集抽象域的可靠浮点实现方法,阐述了如何应用基于该抽象域的浮点实现对浮点程序进行可靠分析.基于抽象解释框架,设计实现了一个面向浮点C程序的静态分析工具原型,并使用浮点实现的区间幂集抽象域对一些浮点程序进行分析.

关键词：浮点程序、静态分析、抽象解释、区间幂集

分类号：TP311.13(计算技术、计算机技术)

在线出版日期：2013-03-28（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：209-217