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.
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).
We are looking for partners and contributors to the OpenSource development of NuSMV. If you would like to
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 institutions currently involved in the development of NuSMV are: