NuSMV
In computer science, NuSMV is a reimplementation and extension of the SMV symbolic model checker, the first model checking tool based on binary decision diagrams (BDDs). The tool has been designed as an open architecture for model checking. It is aimed at reliable verification of industrially sized designs, for use as a backend for other verification tools and as a research tool for formal verification techniques. NuSMV has been developed as a joint project between ITC-IRST ( in Trento), Carnegie Mellon University, the University of Genoa and the University of Trento. NuSMV 2, version 2 of NuSMV, inherits all the functionalities of NuSMV. Furthermore, it combines BDD-based model checking with SAT-based model checking. It is maintained by Fondazione Bruno Kessler, the successor organization of ITC-IRST. Functionalities 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. Running NuSMV Interactively The interaction shell of NuSMV is activated from the system prompt as follows: [system_prompt]$ NuSMV -int NuSMV> go NuSMV> 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.