位置:成果数据库 > 期刊 > 期刊详情页
单变量区间线性不等式抽象域
  • ISSN号:0254-4164
  • 期刊名称:《计算机学报》
  • 时间:0
  • 分类:TP301[自动化与计算机技术—计算机系统结构;自动化与计算机技术—计算机科学与技术]
  • 作者机构:[1]国防科学技术大学计算机学院并行与分布处理国防科技重点实验室,长沙410073
  • 相关基金:国家自然科学基金(60725206 60621003 60673118); 湖南省自然科学基金(07JJ1011)资助
中文摘要:

程序变量的值范围信息对于编译器优化、程序分析与验证等应用至关重要.抽象解释理论提供了一种通用框架为程序变量计算近似的但是可靠的值范围.然而该框架下已有的数值抽象域在表达非凸性质方面存在一定的局限性,影响了值范围分析的精度.文中基于抽象解释理论,提出一个新的数值抽象域——单变量区间线性不等式抽象域.其主要思想是使用单变量区间线性不等式约束作为域元素的约束表示方法.该抽象域的表达能力强于经典的区间抽象域,并允许表达某类非凸、非连通性质.同时,其域操作存在高效的实现算法.该抽象域具有很强的可扩展性,能够应用在实际大规模的程序分析中.

英文摘要:

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-variable interval linear inequality constraints as the representation of domain elements.The new domain is more expressive than the classic interval abstract domain and allows expressing certain non-convex,unconnected properties.Moreover,its domain operations can be implemented via efficient algorithms.Thus,it has high scalability and can be applied in large-scale program analysis in practice.

同期刊论文项目
期刊论文 25 会议论文 10
同项目期刊论文
期刊信息
  • 《计算机学报》
  • 北大核心期刊(2011版)
  • 主管单位:中国科学院
  • 主办单位:中国计算机学会 中国科学院计算技术研究所
  • 主编:孙凝晖
  • 地址:北京中关村科学院南路6号
  • 邮编:100190
  • 邮箱:cjc@ict.ac.cn
  • 电话:010-62620695
  • 国际标准刊号:ISSN:0254-4164
  • 国内统一刊号:ISSN:11-1826/TP
  • 邮发代号:2-833
  • 获奖情况:
  • 中国期刊方阵“双效”期刊
  • 国内外数据库收录:
  • 美国数学评论(网络版),荷兰文摘与引文数据库,美国工程索引,美国剑桥科学文摘,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊(2004版),中国北大核心期刊(2008版),中国北大核心期刊(2011版),中国北大核心期刊(2014版),中国北大核心期刊(2000版)
  • 被引量:48433