NuSMV: a new symbolic model checker NuSMV is a symbolic model checker developed as a joint project between: The Embedded Systems Unit in the Digital Industry Center at FBK-IRST The Model Checking group at Carnegie Mellon University, the Mechanized Reasoning Group at University of Genova The Mechanized Reasoning Group at University of Trento. NuSMV is a reimplementation and extension of SMV1, the f