This chapter gives an overview of model checking, focusing on the verification of concurrent, distributed software systems by means of the SP I N model checker. After discussing S P I N’s input languages, more details are given on the verification flow and on how to improve the verification performance. The discussion is complemented by a practical example concerning the verification of an interactive consistency protocol. The chapter ends with a small number of references, which are useful as a starting point for further reading.