The chapter introduces symbolic model checking as an alternative to extensive simulation and other verification techniques, highlighting its efficiency and ability to handle large state spaces. Symbolic model checking uses temporal logic formulas to specify properties of systems represented by state-transition graphs. The approach employs binary decision diagrams to implicitly represent the transition relation, allowing for verification of systems with up to $10^{20}$ states. Key advantages include automation, the ability to provide counterexamples, and the capability to verify partially specified systems. The Symbolic Model Verifier (SMV) is a widely used tool that has successfully verified various industrial systems. The chapter also covers the SMV language for describing systems, the use of computation tree logic (CTL) for specifying properties, and extensions to the technique, such as timing analysis, word-level model checking, and compositional reasoning.The chapter introduces symbolic model checking as an alternative to extensive simulation and other verification techniques, highlighting its efficiency and ability to handle large state spaces. Symbolic model checking uses temporal logic formulas to specify properties of systems represented by state-transition graphs. The approach employs binary decision diagrams to implicitly represent the transition relation, allowing for verification of systems with up to $10^{20}$ states. Key advantages include automation, the ability to provide counterexamples, and the capability to verify partially specified systems. The Symbolic Model Verifier (SMV) is a widely used tool that has successfully verified various industrial systems. The chapter also covers the SMV language for describing systems, the use of computation tree logic (CTL) for specifying properties, and extensions to the technique, such as timing analysis, word-level model checking, and compositional reasoning.