| 《计算机学报》文章摘要 全文下载 | |
| 文章题目 | 单变量区间线性不等式抽象域 |
| 作者 | 陈立前 王戟 侯苏宁 |
| 作者单位 | (国防科学技术大学计算机学院并行与分布处理国防科技重点实验室 长沙 410073) |
| 发表年份 | 2010 |
| 发表月份 | 3期(427—439) |
| 文章摘要 | 摘要 程序变量的值范围信息对于编译器优化、程序分析与验证等应用至关重要.抽象解释理论提供了一种通用框架为程序变量计算近似的但是可靠的值范围.然而该框架下已有的数值抽象域在表达非凸性质方面存在一定的局限性,影响了值范围分析的精度.文中基于抽象解释理论,提出一个新的数值抽象域——单变量区间线性不等式抽象域.其主要思想是使用单变量区间线性不等式约束作为域元素的约束表示方法.该抽象域的表达能力强于经典的区间抽象域,并允许表达某类非凸、非连通性质.同时,其域操作存在高效的实现算法.该抽象域具有很强的可扩展性,能够应用在实际大规模的程序分析中. 关键词 值范围分析;静态分析;抽象解释;抽象域;区间分析 中图法分类号 TP301 DOI号: 10.3724/SP.J.1016.2010.00427 |