10.3969/j.issn.1007-130X.2017.04.018
一个基于两区间八边形约束的抽象域
抽象解释静态程序分析技术用来发现运行时错误,保证程序正确性,已经被成功应用到工业界.抽象域是抽象解释理论中的一个重要方面,然而大部分已存在的数值抽象域无法表示程序的非凸性质,抽象域的这种凸性限制很多时候会影响数值分析的精度,甚至带来更多误报.基于两区间八边形约束,提出了一个新的数值抽象域,其约束形式为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