一个基于两区间八边形约束的抽象域

摘要：

抽象解释静态程序分析技术用来发现运行时错误,保证程序正确性,已经被成功应用到工业界.抽象域是抽象解释理论中的一个重要方面,然而大部分已存在的数值抽象域无法表示程序的非凸性质,抽象域的这种凸性限制很多时候会影响数值分析的精度,甚至带来更多误报.基于两区间八边形约束,提出了一个新的数值抽象域,其约束形式为z±y∈[a,b]U[c,d],其中x和y表示变量取值,a,b,c,d∈R.该抽象域的域元素是用两区间八边形约束表示,因此可以表达某类非凸性质,表达能力强于经典的八边形抽象域,并且相对于八边形抽象域,域操作的计算复杂度并没有提高太多.

关键词：抽象解释、八边形抽象域、两区间、迁移函数

所属期刊栏目：39

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

资助基金：国家863计划2015AA015303;江苏省研究生培养创新工程KYLX_0315;国家自然科学基金61272038

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

页数：共8页

页码：740-747