We are happy to announce the availability of the first snapshot version of
the new GUI built on the top of the NuSMV 2 model checker.
gNuSMV-snapshot-021002 is available from
Notice that this is *not* a release version yet, but it is a snapshot of the
development branch. This means that many functionalities are still to be
developed, and others do not fully work, but users can start using basic model
checking functionalities and hopefully supply feedback.
With respect to the old GUI, developed for NuSMV 1 and no longer
maintained for NuSMV 2, gNuSMV gives support to several new features
and improvements we recently implemented into NuSMV 2, in particular:
- Support for past temporal operators and for strong fairness in
- Bounded Model Checking
- Based on NuSMV 2.1.0, the latest major release of NuSMV.
Due to licensing restriction, we had to drop the ZCHAFF
support, in order to keep aligned both the Linux and Windows versions.
- Design takes into account extensibility.
The Model-View-Controller pattern and the high modularity
allow easier extensibility and reuse.
The GUI code is fully based on Python, a high-level object oriented scripting
language, which also allows a very rapid prototyping and development process.
Both the graphic toolkit GTK2 and Python are easily portable
under as many platforms as NuSMV 2 supports, with no need of recompilation.
However, the installation of the snapshot might require some
preliminary work of installation of the required packages on
We currently provide versions for Linux and Windows operating systems.
To download and install the version you are interested in, follow these links:
and NuSMV version 2
2 in short) are licensed under the
GNU Lesser General Public License (LGPL in short).
The aim of the NuSMV OpenSource project is to allow the whole model checking
community to participate to the development of NuSMV. To this purpose, we
have chosen a license that:
- is "copyleft", that is, it requires that anyone who improves the
system has to make the improvements freely available;
- permits to use the system in research and commercial applications,
In brief, the LGPL license allows anyone to freely download, copy, use, modify,
and redistribute (g)NuSMV 2, proviso that any modification and/or extension
to the library is made publicly available under the terms of LGPL.
The license also allows the usage of the (g)NuSMV 2 as part of a larger software
system *without* being obliged to distributing the whole software under LGPL.
Also in this case, the modification to (g)NuSMV 2 (*not* to the larger software)
should be made available under LGPL.
The precise terms and conditions for copying, distribution and modification
can be found in file LGPL-2.1. You can contact <email@example.com>
if you have any doubt or comment on the license.
Different partners have participated the initial release of NuSMV 2. Every
source file in the (g)NuSMV 2 distribution contains a header that acknowledges
the developers and the copyright holders for the file. In particular:
- CMU and ITC-IRST contributed the source code on NuSMV version
- ITC-IRST has also developed several extensions for NuSMV 2;
- ITC-IRST has also developed gNuSMV, the GUI edition for NuSMV
- ITC-IRST and the University of Trento have developed the SAT-based
Bounded Model Checking package on NuSMV 2;
- University of Genova has contributed SIM, a state-of-the-art SAT
solver, and the RBC package use in the Bounded Model Checking algorithms.
The NuSMV team has also received several contributions for different part
of the system. In particular:
- Ariel Fuxman <firstname.lastname@example.org> has extended the LTL
to SMV tableau translator to the past fragment of LTL
- Rik Eshuis <email@example.com> has contributed a strong
fairness model checking algorithm for LTL specifications
- Dan Sheridan <firstname.lastname@example.org> has contributed
several extensions and enhancements to the Bounded Model Checking algorithms.