We are happy to announce the availability of the first snapshot version of gNuSMV,
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 LTL
  • 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.
  • Portability
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 your machine.


The welcome pageWelcome page The Modeling viewModeling view
The Properties viewProperties list The Traces viewTraces view


We currently provide versions for Linux and Windows operating systems.
To download and install the version you are interested in, follow these links:
Linux version
Windows version


Both gNuSMV and NuSMV version 2(NuSMV 2 in short) are licensed under the
GNU Lesser General Public License (LGPL in short).
For a complete information about LGPL visit URL<>.

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:
  1. is "copyleft", that is, it requires that anyone who improves the system has to make the improvements freely available;
  2. permits to use the system in research and commercial applications, without restrictions. 

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 <> 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 1;
  • ITC-IRST has also developed several extensions for NuSMV 2;
  • ITC-IRST has also developed gNuSMV, the GUI edition for NuSMV 2;
  • 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 <> has extended the LTL to SMV tableau translator to the past fragment of LTL
  • Rik Eshuis <> has contributed a strong fairness model checking algorithm for LTL specifications
  • Dan Sheridan <> has contributed several extensions and enhancements to the Bounded Model Checking algorithms.