NuSMV

NuSMV is an updated version of the SMV symbolic model checker.

NuSMV has been developed as a joint project between ITC-IRST (Istituto Trentino di Cultura, Istituto per la Ricerca Scientifica e Tecnologica in Trento, Italy), Carnegie Mellon University, the University of Genoa and the University of Trento. It is a reimplementation and extension of SMV, the first model checker 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 2 is open source software. It combines BDD-based model checking with SAT-based model checking.