谓词抽象技术中循环反例的解决方法研究

摘要：

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

关键词：模型检测、谓词抽象、求精、反例、循环

所属期刊栏目：31

分类号：TP391(计算技术、计算机技术)

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

页数：共5页

页码：5269-5272,5277