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

• 作者: 姜加红 王戟 陈立前
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: 浮点程序 静态分析 抽象解释 区间幂集
• 年，卷（期）: 2013,（3）
• 页码范围: 209-217
• 分类号: TP311.13
• 字数: 7558字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.1209023

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王戟	国防科学技术大学计算机学院	44	1257	17.0	35.0
2	陈立前	国防科学技术大学计算机学院	10	43	4.0	6.0
3	姜加红	国防科学技术大学计算机学院	1	5	1.0	1.0