Description:

NuSMV is a reimplementation and extension of SMV, the first model
checker based on BDDs. NuSMV has been designed to be an open
architecture for model checking, which can be reliably used for the
verification of industrial designs, as a core for custom verification
tools, as a testbed for formal verification techniques, and applied
to other research areas.

NuSMV2, combines BDD-based model checking component that exploits the
CUDD library developed by Fabio Somenzi at Colorado University and
SAT-based model checking component that includes an RBC-based Bounded
Model Checker, connected to the SIM SAT library developed by the
University of Genova.