Bounded Model Checking Using Satisfiability Solving

This tutorial focuses on recent techniques that combine model checking with satisfiability solving, known as bounded model checking, which do a very fast exploration of the state space, and for some types of problems seem to offer large performance improvements over previous approaches.