谓词抽象技术中循环反例的解决方法研究
Research of solving counterexamples with loops in predicate abstraction technology作者机构：解放军信息工程大学电子技术学院河南郑州450004
出 版 物：《计算机工程与设计》 (Computer Engineering and Design)
年 卷 期：2010年第31卷第24期
页 面：5269-5272,5277页
学科分类：081203[工学-计算机应用技术] 08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）]
摘 要：为了解决谓词抽象技术面临的程序中循环体的每次迭代都至少需要一个谓词来实现的难题,提出了一个两阶段的不完全判定过程,用来对一个包含循环的反例进行可行性模拟。通过给出的循环探测算法来从抽象模型中提取出包含循环的反例,并用循环迭代的数量作为参数来确定模拟实例。实验结果表明,该方法在典型的缓冲溢出实例中的表现优于传统的抽象求精方法。
维普期刊数据库
同方期刊数据库