Many problems in computer science can be reduced to checking the satisfiability of a formula in some logic. Several of these problems can be naturally formulated as Satisfiability Modulo Theories (SMT) problems, where one is interested in the satisfiability of first-order formulas with respect to some logical theory T. Examples of such theories include several forms of arithmetic as well as various theories of strings, arrays, records, algebraic data types, finite sets, and finite relations. SMT differs from traditional automated deduction mainly for using specialized inference methods for each theory T. By being theory-specific and restricted to certain classes of formulas, these methods can be implemented in solvers that are considerably more efficient in practice than general-purpose theorem provers. SMT solvers have been used successfully as backend reasoning engines in a very large, and still growing, number of application areas. These include hardware verification and equivalence checking, bounded and unbounded model checking, program verification, security analysis, symbolic execution, automated test case generation, automated exploit generation, type checking, compilation validation, invariant synthesis, program synthesis, configuration synthesis, design space exploration, planning, and scheduling, among others. This tutorial will give a general overview of SMT and the inner workings of SMT solvers, and illustrate how SMT is contributing to advance the state of the art in some of the applications areas above.