smt求解技术简述 brief introduction to smt solving.pdfVIP

金继伟，马菲菲，张 健.SMT求解技术简述[J].计算机科学与探索，2015 ，9（7 ）：769-780. ISSN 1673-9418 CODEN JKYTA8 E-mail: fcst@vip. 163.com Journal of Frontiers of Computer Science and Technology 1673-9418/2015/09(07)-0769-12 Tel: +86-10 doi: 10.3778/j.issn. 1673-9418.1405041 SMT 求解技术简述* + 金继伟 ，马菲菲，张 健 中国科学院 软件研究所，北京 100190 Brief Introduction to SMT Solving + JIN Jiwei , MA Feifei, ZHANG Jian Institute of Software, Chinese Academy of Sciences, Beijing 100190, China + Corresponding author: E-mail: jinjw@ JIN Jiwei, MA Feifei, ZHANG Jian. Brief introduction to SMT solving. Journal of Frontiers of Computer Science and Technology, 2015, 9(7) ：769-780. Abstract: SMT is the problem of deciding the satisfiability of a first order formula with respect to some theory formulas. It is being recognized as increasingly important due to its applications in different communities, in particular in formal verification, program analysis and software testing. This paper provides a brief overview of SMT and its theories. Then this paper introduces some approaches aiming to improve the efficiency of SMT solving, including eager and lazy approaches and optimum technique which have been proposed in the last ten years. This paper also introduces some state-of-the-art SMT solvers, including Z3, Yices and CVC3/CVC4. Finally, this paper gives a preliminary prospect on the research trends of SMT, which include SMT with quantifier, optimization problems subject to SMT and volume computation for SMT. Key words: satisfiability modulo theories (SMT); DPLL(T); solver 摘 要：SMT 问题是在特定理论下判定一阶逻辑公式可满足性问题。它在很多领域，尤其是形式验证、程序分 析、软件测试等领域，都有重要的应用。介绍了SMT 问题的基本概念、相关定义以及目前