| SMT求解技术简述 |
| |
| 引用本文： | 金继伟,马菲菲,张健.SMT求解技术简述[J].计算机科学与探索,2015(7). |
| |
| 作者姓名： | 金继伟 马菲菲 张健 |
| |
| 作者单位： | 中国科学院 软件研究所,北京,100190 |
| |
| 摘 要： | SMT问题是在特定理论下判定一阶逻辑公式可满足性问题。它在很多领域，尤其是形式验证、程序分析、软件测试等领域，都有重要的应用。介绍了SMT问题的基本概念、相关定义以及目前的主流理论。近年来出现了很多提高SMT求解效率的技术，着重介绍并分析了这些技术，包括积极类算法、惰性算法及其优化技术等。介绍了目前的主流求解器和它们各自的特点，包括Z3、Yices、CVC3/CVC4等。对SMT求解技术的前景进行了展望，量词的处理、优化问题和解空间大小的计算等尤其值得关注。
|
| 关 键 词： | 可满足性模理论(SMT) DPLL(T) 求解器 |
Brief Introduction to SMT Solving |
| |
| JIN Jiwei,MA Feifei,ZHANG Jian.Brief Introduction to SMT Solving[J].Journal of Frontier of Computer Science and Technology,2015(7). |
| |
| Authors: | JIN Jiwei MA Feifei ZHANG Jian |
| |
| Abstract: | |
| |
| Keywords: | satisfiability modulo theories(SMT) DPLL(T) solver |
| 本文献已被 万方数据 等数据库收录！ |
|
