SMT求解器理论组合技术研究

• 作者: 刘万伟 李婧
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 可满足模理论 SMT求解器 组合理论
• 年，卷（期）: 2011,（10）
• 所属期刊栏目: 软件工程
• 页码范围: 111-119
• 分类号: TP301
• 字数: 8063字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2011.10.020

摘要

可满足模理论(SMT)求解器是计算机科学中用来判定一阶逻辑公式可满足性的程序,是许多形式化方法的验证引擎.理论求解器实现了SMT基于不同理论背景的求解过程,然而实际问题常以多个理论为背景.因此,本文重点介绍理论组合判定方法,概述SMT求解器的发展现状,并分析了几个主流SMT求解器理论组合判定关键技术.通过对照实验,评估各组合判定方法的优缺点以及目前流行的支持理论组合SMT求解器在工业应用中的性能.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘万伟		3	30	3.0	3.0
2	李婧		1	18	1.0	1.0