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.
金继伟，马菲菲，张健. SMT求解技术简述[J]. 计算机科学与探索, 2015, 9(7): 769-780.DOI:10.3778/j.issn.1673-9418.1405041.
JIN Jiwei, MA Feifei, ZHANG Jian. Brief Introduction to SMT Solving. Journal of Frontiers of Computer Science and Technology, 2015, 9(7): 769-780.DOI:10.3778/j.issn.1673-9418.1405041.