NuSMV: 2.54 - A Symbolic Model Checker

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, which can
be connected to the Minisat SAT Solver and/or to the ZChaff SAT Solver. The
University of Genova has contributed SIM, a state-of-the-art SAT solver used
until version 2.5.0, and the RBC package use in the Bounded Model Checking
algorithms.