Model checking and testing have a lot in common. Over the last two
decades, significant progress has been made on how to broaden the
scope of model checking from finite-state abstractions to actual
software implementations. One way to do this consists of adapting
model checking into a form of systematic testing that is applicable to
industrial-size software. This chapter presents an overview of this
strand of software model checking.