Satisfiability Modulo Theories (SMT) studies methods for checking the satisfiability of first-order formulas with theories. SMT solvers are now a core tool in many areas like planning, security testing, automated test generation, and all kinds of verification tasks. In contrast to other related areas, the leading SMT solvers are almost exclusively developed as open-source projects.
Satisfiability Modulo Theories is the decision problem of whether a first-order formula with background theories, such as real or integer arithmetic, bit-vectors, floating-points, or strings, is satisfiable. In its comparably short history of roughly 20 years, it managed to deliver both great expressive power and strong practical performance. Moreover, most solvers are developed as open-source projects which allows newcomers to contribute more easily.
We review the basics of Satisfiability Modulo Theories solving and present some of the most prominent solvers before highlighting a few of the numerous success stories of SMT solvers being applied in practice. Well-known users include Amazon and Microsoft, as well a huge number of smaller companies and projects from various backgrounds.
This talk targets anyone that occasionally confronts hard-to-solve problems: Satisfiability Modulo Theories is a mature industrial-grade solving technology that might just solve your problem with little effort on your part.