论文部分内容阅读
为了解决谓词抽象技术面临的程序中循环体的每次迭代都至少需要一个谓词来实现的难题,提出了一个两阶段的不完全判定过程,用来对一个包含循环的反例进行可行性模拟。通过给出的循环探测算法来从抽象模型中提取出包含循环的反例,并用循环迭代的数量作为参数来确定模拟实例。实验结果表明,该方法在典型的缓冲溢出实例中的表现优于传统的抽象求精方法。