The field of model checking owes much of its great success and impact to the use of symbolic techniques to reason efficiently about functional properties of hardware or software systems. Traditionally, these techniques have relied on propositional encodings of transition systems and on propositional reasoning engines such as binary decision diagrams and SAT solvers. More recently, a number of these techniques have been adapted, and new ones have been devised, based instead on encodings into fragments of first-order logic supported by Satisfiability Modulo Theories (SMT) solvers. These are highly efficient solvers specialized on checking the satisfiability of formulas in certain logical theories such as the theory of linear arithmetic, bit-vectors, arrays, algebraic data types, and so on. SMT-based model checking methods blur the line between traditional (propositional) model checking and traditional (first or higher order) deductive verification. More crucially, they combine the best features of both by offering the scalability and scope of deductive verification while maintaining comparable levels of automations as propositional model checking.

This talk will briefly introduce SMT and then give an overview of SMT-based model checking, focusing on a number of notable approaches and techniques.