摘要
软件模型检验面临的难题是状态空间爆炸问题。解决此问题的重要方法是谓词抽象。在传统的反例导向精化方法中,谓词抽象是通过调用定理证明器计算抽象程序,然而计算效率不高,因此引入了SAT求解器计算抽象程序。通过具体迁移关系的布尔公式构造,用SAT计算抽象程序的方法,包括基本块和控制流语句抽象迁移关系的构造,完成基于SAT抽象程序构造方法的优势。实例分析表明,基于SAT的谓词抽象技术是一种构造程序抽象模型更高效的方法。
State space explosion is the key problem in software model checking. A critical technology for solving the problem is predicate abstraction. In the traditional counterexample-guided abstraction refinement （CEGAR）, predicate abstraction computes abstract program by calling theorem prover, which is low in efficiency. SAT solver is thus introduced. This paper first presents the construction of the Boolean formula of concrete transition relation. Then computes the abstract program using SAT, which includes constructing the abstract relation of basic block and control flow statement. Finally advantages of this method are summarized. Example analysis shows that the SAT-based predicate abstraction technology is a more efficient method for constructing program abstract model.
出处
《桂林电子科技大学学报》
2008年第5期407-411,共5页
Journal of Guilin University of Electronic Technology
基金
国家自然科学基金(60663005)
广西自然科学青年基金(0542036
0728093)
关键词
模型检验
谓词抽象
抽象求精
SAT
model checking
predicate abstraction
abstraction refinement
SAT
