Symbolic model checking is a powerful formal specification and verification method that has been successfully applied in various industrial designs. It allows the verification of large finite-state systems, with state spaces up to $10^{30}$ states being exhaustively searched in minutes. Models with more than $10^{120}$ states have been verified using special techniques. This approach uses symbolic algorithms, which represent the transition relation implicitly through boolean formulas and binary decision diagrams, resulting in a much smaller representation and enabling the verification of extremely large state spaces. Symbolic model checking offers several advantages, including automatic verification without user intervention, providing counterexamples when formulas are not satisfied, and the ability to verify partially specified systems. It also allows for the verification of systems concurrently with their design, providing valuable hints for error elimination and system improvement. The system being verified is described in the SMV language, which supports synchronous and asynchronous, detailed deterministic and abstract nondeterministic finite state machines. It provides modular hierarchical descriptions, component reuse, and parameterization. The SMV program can be viewed as a system of simultaneous equations whose solution determines the next state. Fairness constraints can also be specified in SMV, allowing verification to be restricted to fair paths. Computation tree logic (CTL) is used by SMV to express properties that will be verified. CTL formulas are built from atomic propositions, boolean connectives, and temporal operators. The most common CTL operators include AG, AF, and EF, which express different types of properties. Examples of CTL formulas illustrate the expressiveness of the logic. Symbolic model checking has been applied successfully in various industrial systems, including the Futurebus+ cache coherence protocol, the PCI Local Bus, a railway signaling system, an aircraft controller, a manufacturing system, and a medical monitoring system. The technique has been further extended to include timing properties, word-level model checking, symmetry, abstraction, and compositional reasoning, significantly enhancing its power. More information about SMV and the model checker can be found at http://www.cs.cmu.edu/~modelcheck.Symbolic model checking is a powerful formal specification and verification method that has been successfully applied in various industrial designs. It allows the verification of large finite-state systems, with state spaces up to $10^{30}$ states being exhaustively searched in minutes. Models with more than $10^{120}$ states have been verified using special techniques. This approach uses symbolic algorithms, which represent the transition relation implicitly through boolean formulas and binary decision diagrams, resulting in a much smaller representation and enabling the verification of extremely large state spaces. Symbolic model checking offers several advantages, including automatic verification without user intervention, providing counterexamples when formulas are not satisfied, and the ability to verify partially specified systems. It also allows for the verification of systems concurrently with their design, providing valuable hints for error elimination and system improvement. The system being verified is described in the SMV language, which supports synchronous and asynchronous, detailed deterministic and abstract nondeterministic finite state machines. It provides modular hierarchical descriptions, component reuse, and parameterization. The SMV program can be viewed as a system of simultaneous equations whose solution determines the next state. Fairness constraints can also be specified in SMV, allowing verification to be restricted to fair paths. Computation tree logic (CTL) is used by SMV to express properties that will be verified. CTL formulas are built from atomic propositions, boolean connectives, and temporal operators. The most common CTL operators include AG, AF, and EF, which express different types of properties. Examples of CTL formulas illustrate the expressiveness of the logic. Symbolic model checking has been applied successfully in various industrial systems, including the Futurebus+ cache coherence protocol, the PCI Local Bus, a railway signaling system, an aircraft controller, a manufacturing system, and a medical monitoring system. The technique has been further extended to include timing properties, word-level model checking, symmetry, abstraction, and compositional reasoning, significantly enhancing its power. More information about SMV and the model checker can be found at http://www.cs.cmu.edu/~modelcheck.