NUSMV is the result of the reengineering, reimplementation and
extension of SMV , version 2.4.4 (SMV from now
on). With respect to SMV, NUSMV has been extended and upgraded
along three dimensions.
First, from the point of view of the system functionalities, NUSMV
features a textual interaction shell and a graphical interface,
extended model partitioning techniques, and allows for LTL model
Second, the system architecture of NUSMV has been designed to be
highly modular and open. The interdependencies between different
modules have been separated, and an external, state of the art BDD
package  has been integrated in the system kernel.
Third, the quality of the implementation has been strongly enhanced.
This makes of NUSMV a robust, maintainable and well documented
system, with a relatively easy to modify source code.
NUSMV is available at