| SMT求解器理论组合技术研究 |
| |
| 引用本文： | 李婧,刘万伟.SMT求解器理论组合技术研究[J].计算机工程与科学,2011,33(10):111-119. |
| |
| 作者姓名： | 李婧 刘万伟 |
| |
| 作者单位： | 并行与分布处理国防科技重点实验室,湖南长沙,410073 |
| |
| 基金项目： | 国家自然科学基金重点项目软件工程学 |
| |
| 摘 要： | 可满足模理论(SMT)求解器是计算机科学中用来判定一阶逻辑公式可满足性的程序,是许多形式化方法的验证引擎.理论求解器实现了SMT基于不同理论背景的求解过程,然而实际问题常以多个理论为背景.因此,本文重点介绍理论组合判定方法,概述SMT求解器的发展现状,并分析了几个主流SMT求解器理论组合判定关键技术.通过对照实验,评估...
|
| 关 键 词： | 可满足模理论 SMT求解器 组合理论 |
A Survey on Theoretical Combination Techniques of SMT Solvers |
| |
| LI Jing,LIU Wan-wei.A Survey on Theoretical Combination Techniques of SMT Solvers[J].Computer Engineering & Science,2011,33(10):111-119. |
| |
| Authors: | LI Jing LIU Wan-wei |
| |
| Abstract: | 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 applications often are supported by multiple theories.This paper mainly introduces the methods of theory combination,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. |
| |
| Keywords: | satisfiability modulo theories SMT solver combination theory |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与科学》浏览原始摘要信息 |
|
点击此处可从《计算机工程与科学》下载全文 |
|
