摘要
可满足模理论(SMT)求解器是计算机科学中用来判定一阶逻辑公式可满足性的程序,是许多形式化方法的验证引擎。理论求解器实现了SMT基于不同理论背景的求解过程,然而实际问题常以多个理论为背景。因此,本文重点介绍理论组合判定方法,概述SMT求解器的发展现状,并分析了几个主流SMT求解器理论组合判定关键技术。通过对照实验,评估各组合判定方法的优缺点以及目前流行的支持理论组合SMT求解器在工业应用中的性能。
Satisfiability modulo theories solver is a decision procedure for the satisfiabilily of formulas of the first-order logics. It is the verification engine for many formalization methods. Theory solvers solve problems with different theoretical backgrounds; however, the problems in the real-world applica- tions often are supported by multiple theories. This paper mainly introduces the methods of theory com- bination, summarizes the status quo of the SMT solvers. Besides,it analyzes several major techniques on the theoretical combination for SMT solvers. Testing with the industrial cases, we finally evaluate methods of combination theory with experimental results, and compare the performances of several popular SMT solvers which support theoretical combination techniques.
出处
《计算机工程与科学》
CSCD
北大核心
2011年第10期111-119,共9页
Computer Engineering & Science
基金
国家自然科学基金重点项目软件工程学(0904067107002)
关键词
可满足模理论
SMT求解器
组合理论
satisfiability modulo theories
SMT solver
combination theory
