Satisfiability Modulo Theories (SMT) is concerned with the problem of determining the satisfiability of first-order formulas with respect to a given logical theory T . A distinguishing feature of SMT is the use of inference methods tailored to the particular theory T . By being theory-specific and restricting their language to certain classes of formulas (such as, typically but not exclusively, ground formulas), such methods can be implemented into solvers that are more efficient in practice than general-purpose theorem provers. SMT techniques have been traditionally developed to support deductive software verification, but they have also applications in model checking, certifying compilers, automated test generation, and other formal methods. This talk gives an overview of SMT and its applications, and highlights some long-standing challenges for a wider applications of SMT techniques within formal methods, as well as some fresh challenges introduced by new potential uses. A major challenge is providing adequate model generation features for disproving verification conditions.