OpenSource NuSMV

Enormous progress has been carried out over the last decade in the applicability of symbolic model checking to practical verification problems. However, most of the state-of-the-art model checkers are proprietary. This is a clear disadvantage in terms of scientific progress, and is slowing down the introduction of model checking in non-traditional application domains. We are starting the NuSMV OpenSource project, for the development of a publicly available, state-of-the-art symbolic model checker.

The NuSMV OpenSource development project

With the OpenSource model, a whole community participated in the development of a software systems, with a distributed tean and independent peer review, and results in a rapid systems evolution, and increased software quality and reliability. The OpenSource model has boosted the take-up of notable software systems, such as Linux and Apache. With the NuSMV OpenSource project, we would like to reach the same goals within the model checking community, opening the development of NuSMV. The new versions of NuSMV will be distributed under GNU Lesser General Public License 2.1 (LGPL).

  • LGPL grants full right to use and modify NuSMV for research and commercial applications.

  • LGPL is copyleft: any development is required to fall under the same license, thus becoming available to the whole community.

Join the NuSMV OpenSource development project!

We are looking for partners and contributors to the OpenSource development of NuSMV. If you would like to

  • develop a new functionality or an improvement,

  • ask for an extension to NuSMV,

  • request information or simply state your opinion,
please email the NuSMV users mailling list . News will also be available on the NuSMV web site.

NuSMV v2: BDD+SAT based model checking

NuSMV is a reimplementation/extension of SMV, and has been designed to be a robust, well documented, open platform for model checking. The starting point of the OpenSource development of NuSMV is NuSMV2, that combines BDD-based model checking component that exploits the CUDD library developed by Fabio Somenzi at Colorado University and the 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.

NuSMV2 presents other new features: for instance, it allows for a more powerful manipulation of multiple models; it can generate flat models for the whole language; it allows for cone of influence reduction.

The NuSMV development team

The institutions currently involved in the development of NuSMV are:

  • IRST (Trento, Italy), as the co-developer of NuSMV and main developer of NuSMV2.

  • CMU (Pittsburgh, PA), as the co-developer of NuSMV.

  • The University of Genova (Italy), as the developer of state-of-the-art SAT technology.

  • The University of Trento (Italy), as the co-developer of the bounded model checker.
Ken McMillan (Cadence) has expressed an interest in contributing to the project with the improvements that have been carried out on Cadence SMV along the years. Statements of interest have also come from several other commercial and academic institutions.

Useful links

NuSMV <>