多面体抽象域的整数实现方法及其在程序分析中的应用[EB/OL]
北京：中国科技论文在线
） 摘要： 抽象解释理论为静态程序分析提供了一个通用框架
抽象域是该框架下的核心
多面体抽象域可用来产生线性不等式,是目前表达能力最强、应用最广泛的数值抽象域之一
现有的多面体抽象域实现一般采用多精度有理数,在实际应用中可扩展性方面受到限制
本文采用多面体抽象域基于约束的表示方法,给出了多面体抽象域的一种基于机器整数的实现方法
为了提高基于机器整数实现的多面体抽象域的可扩展性,本文提出了一些策略来限制约束系数的大小和约束的个数;另一方面,针对目标程序是整数程序的情况,本文根据变量的整数特点,提出了一些优化方法提高分析精度
实验表明,与基于多精度有理数实现的多面体抽象域相比,基于机器整数实现的多面体抽象域计算效率更高,并且更适合整数程序分析
程序分析 【收录情况】 中国科技论文在线： 田楠
