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

作     者：梁加宾 张来顺 LIANG Jia-bin;ZHANG Lai-shun

作者机构：解放军信息工程大学电子技术学院河南郑州450004 

出 版 物：《计算机工程与设计》 (Computer Engineering and Design)

年 卷 期：2010年第31卷第24期

页      码：5269-5272,5277页

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

主 题 词：模型检测 谓词抽象 求精 反例 循环 

学科分类：081203[081203] 08[工学] 0835[0835] 0812[工学-测绘类] 

D　O　I：10.16208/j.issn1000-7024.2010.24.029

馆 藏 号：203195306...