NuSMV: a new symbolic model checker

NuSMV is a symbolic model checker developed as a joint project between:

NuSMV is a reimplementation and extension of SMV1, 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.

Latest News

NuSMV 2.7.0 is OUT!

NuSMV 2 is Open Source!

NuSMV 2.6.0 is OUT!

Release Notes

Version 2.7.0 Oct 25, 2024

Version 2.6.0 Oct 14, 2015

Version 2.5.4 Oct 28, 2011

See more

For information about NuSMV, please send an e-mail to . For support or bug reporting write instead to . Please note that we will forward to the latter any technical mail sent to , so to allow all our users to benefit from the answers.