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

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

单位：南京航空航天大学计算机科学与技术学院; 江苏南京210016; 东部战区空军装备部; 江苏南京210018