The process of verifying the correctness of a reactive system consists of establishing that the system behaves as expected. This is usually a crucial task, with key economic significance. Most often, and for hardware systems, the verification of the correct behavior of the system is ensured by model checking. The objective of this talk is to provide a brief tutorial on the verification of reactive systems by model checking. The main topics covered in the talk will be the utilization of model checking in the verification of reactive systems, the syntax and semantics of computation tree logic, the analysis of a simple model checking algorithm, the utilization of symbolic model checking, and the utilization of satisfiability-based model checking algorithms.