[2] It is maintained by Fondazione Bruno Kessler, the successor organization of ITC-IRST.
NuSMV supports the analysis of specifications expressed in CTL and LTL.
It can be run in batch mode, or interactively with a textual user interface.
The interaction shell of NuSMV is activated from the system prompt as follows: NuSMV first tries to read and execute commands from an initialization file if such file exists and is readable unless -s was passed on the command line.
When the initialization phase is completed the NuSMV shell prompt is displayed and the system is now ready to execute user commands.