| 单变量区间线性不等式抽象域 |
| |
| 引用本文： | 陈立前,王戟,侯苏宁.单变量区间线性不等式抽象域[J].计算机学报,2010,33(3). |
| |
| 作者姓名： | 陈立前 王戟 侯苏宁 |
| |
| 作者单位： | 国防科学技术大学计算机学院并行与分布处理国防科技重点实验室,长沙,410073 |
| |
| 基金项目： | 国家自然科学基金(60725206,60621003,60673118);;湖南省自然科学基金(07JJ1011)资助~~ |
| |
| 摘 要： | 程序变量的值范围信息对于编译器优化、程序分析与验证等应用至关重要.抽象解释理论提供了一种通用框架为程序变量计算近似的但是可靠的值范围.然而该框架下已有的数值抽象域在表达非凸性质方面存在一定的局限性,影响了值范围分析的精度.文中基于抽象解释理论,提出一个新的数值抽象域——单变量区间线性不等式抽象域.其主要思想是使用单变量区间线性不等式约束作为域元素的约束表示方法.该抽象域的表达能力强于经典的区间抽象域,并允许表达某类非凸、非连通性质.同时,其域操作存在高效的实现算法.该抽象域具有很强的可扩展性,能够应用在实际大规模的程序分析中.
|
| 关 键 词： | 值范围分析 静态分析 抽象解释 抽象域 区间分析 |
An Abstract Domain of One-Variable Interval Linear Inequalities |
| |
| CHEN Li-Qian,WANG Ji,HOU Su-Ning.An Abstract Domain of One-Variable Interval Linear Inequalities[J].Chinese Journal of Computers,2010,33(3). |
| |
| Authors: | CHEN Li-Qian WANG Ji HOU Su-Ning |
| |
| Affiliation: | National Laboratory for Parallel and Distributed Processing/a>;School of Computer/a>;National University of Defense Technology/a>;Changsha 410073 |
| |
| Abstract: | interpretation provides a general framework to compute statically approximate but sound value ranges for program variables.However,most existing numerical abstract domains under the framework have limitations in expressing non-convex properties,which may lead to imprecision during the value range analysis.This paper proposes a new numerical abstract domain under the framework of abstract interpretation,namely an abstract domain of one-variable interval linear inequalities.The main idea is to use one-variabl... |
| |
| Keywords: | value range analysis static analysis abstract interpretation abstract domain interval analysis |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
