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