基于SAT的程序谓词抽象技术研究

摘要：

软件模型检验面临的难题是状态空间爆炸问题.解决此问题的重要方法是谓词抽象.在传统的反例导向精化方法中,谓词抽象是通过调用定理证明器计算抽象程序,然而计算效率不高,因此引入了SAT求解器计算抽象程序.通过具体迁移关系的布尔公式构造,用SAT计算抽象程序的方法,包括基本块和控制流语句抽象迁移关系的构造,完成基于SAT抽象程序构造方法的优势.实例分析表明,基于SAT的谓词抽象技术是一种构造程序抽象模型更高效的方法.

关键词：模型检验、谓词抽象、抽象求精、SAT

所属期刊栏目：28

分类号：TP311.1(计算技术、计算机技术)

资助基金：国家自然科学基金60663005;广西自然科学青年基金0542036, 0728093

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

页数：共5页

页码：407-411