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

• 作者: 钱俊彦 韦海霞
• 来源期刊: 桂林电子科技大学学报
• 学科: 工学
• 关键词: 模型检验 谓词抽象 抽象求精 SAT
• 年，卷（期）: 2008,（5）
• 所属期刊栏目: 学术论文
• 页码范围: 407-411
• 页数: 5页
• 分类号: TP311.1
• 字数: 5178字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-808X.2008.05.007

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	钱俊彦	桂林电子科技大学计算机与控制学院	86	238	9.0	10.0
2	韦海霞	桂林电子科技大学计算机与控制学院	1	0	0.0	0.0