SAT/SMT solvers and their applications

Abstract

SAT/SMT solvers are currently attracting attentions as convenient backyard engines of many kinds of formal verification/analysis tools. In this article, we explain the current status of those solvers including basic concepts, technical principles, and their useful applications. Technology of SAT solver has great progress in the last decade, and the new technology called SMT solver is also emerged as an influence of them. In the article, we positions these technologies with respect to the relation of formal methods.