This lecture is an introduction to Model Checking
Modulo Theories (MCMT), an new
model checking technique invented by Silvio Ghilardi and Silvio
Ranise. This technique is based on the integration of SMT solving and
backward reachability. We will illustrate the concepts of MCMT
with Cubicle, an open source model
checker for verifying safety properties of array-based systems, a
syntactically restricted class of parametrized transition systems with
states represented as arrays indexed by an arbitrary number of
processes. This lecture will also introduce the main concepts behind
the construction of SMT solvers.