Journal of Software:2008.19(1):27-38

(国防科学技术大学 计算机学院,湖南 长沙 410073)
Advances in Predicate Abstraction
QU Wan-Xia,LI Tun,GUO Yang,YANG Xiao-Dong
Chart / table
Similar Articles
Article :Browse 6157   Download 5544
Received:September 12, 2006    Revised:May 10, 2007
> 中文摘要: 随着软、硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.谓词抽象是解决状态空间爆炸的最有效方法之一,近年来得到迅速发展.介绍了谓词抽象的基本算法并比较了不同的求解支持工具;重点分析了反例指导的抽象求精和基于插值的抽象求精原理;分析了产生新谓词的各种方法的优、缺点;最后指出了谓词抽象技术进一步发展所面临的挑战和发展方向.
中文关键词: 模型检验  谓词抽象  抽象求精  反例  插值
Abstract:With the growing increase in software/hardware system scale and function, the further development and application of model checking has been greatly limited by state space explosion, which becomes the bottleneck of verifying large industrial designs. Predicate abstraction, as one of the most effective ways to address state explosion, has been fueled over the recent years. This paper presents a survey of the latest developments in predicate abstraction. A basic algorithm for predicate abstraction is introduced first, followed by comparison among several solvers. Emphases are put on counterexample-guided abstraction refinement and interpolation-based abstraction refinement, including the principles and improvements. The qualities of the new predicate generation methods are also analyzed. Finally, the major challenges in making this technology more pervasive in industrial design verification domain are noted.
文章编号:     中图分类号:    文献标志码:
基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.60403048, 60573173 (国家自然科学基金) Supported by the National Natural Science Foundation of China under Grant Nos.60403048, 60573173 (国家自然科学基金)
Foundation items:
Reference text:

屈婉霞,李 暾,郭 阳,杨晓东.谓词抽象技术研究.软件学报,2008,19(1):27-38

QU Wan-Xia,LI Tun,GUO Yang,YANG Xiao-Dong.Advances in Predicate Abstraction.Journal of Software,2008,19(1):27-38