首页 | 本学科首页   官方微博 | 高级检索  
     

基于SAT的程序谓词抽象技术研究
引用本文:韦海霞,钱俊彦.基于SAT的程序谓词抽象技术研究[J].桂林电子科技大学学报,2008,28(5).
作者姓名:韦海霞  钱俊彦
作者单位:桂林电子科技大学,计算机与控制学院,广西,桂林,541004
基金项目:国家自然科学基金,广西自然科学青年基金
摘    要:软件模型检验面临的难题是状态空间爆炸问题.解决此问题的重要方法是谓词抽象.在传统的反例导向精化方法中,谓词抽象是通过调用定理证明器计算抽象程序,然而计算效率不高,因此引入了SAT求解器计算抽象程序.通过具体迁移关系的布尔公式构造,用SAT计算抽象程序的方法,包括基本块和控制流语句抽象迁移关系的构造,完成基于SAT抽象程序构造方法的优势.实例分析表明,基于SAT的谓词抽象技术是一种构造程序抽象模型更高效的方法.

关 键 词:模型检验  谓词抽象  抽象求精

SAT-based program predicate abstraction
WEI Hai-xia,QIAN Jun-yan.SAT-based program predicate abstraction[J].Journal of Guilin Institute of Electronic Technology,2008,28(5).
Authors:WEI Hai-xia  QIAN Jun-yan
Abstract:
Keywords:SAT
本文献已被 维普 万方数据 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号