This paper describes a new symbolic model checker, called NuSMV, developed as part of a joint project between CMU and IRST. NuSMV is the result of the reengineering, reimplementation and, to a limited extent, extension of the CMU SMV model checker. The core of this paper consists of a detailed description of the NuSMV functionalities, architecture, and implementation. © 2000 Springer-Verlag.
NUSMV: a new symbolic model checker
Giunchiglia, Fausto;M. Roveri
2000-01-01
Abstract
This paper describes a new symbolic model checker, called NuSMV, developed as part of a joint project between CMU and IRST. NuSMV is the result of the reengineering, reimplementation and, to a limited extent, extension of the CMU SMV model checker. The core of this paper consists of a detailed description of the NuSMV functionalities, architecture, and implementation. © 2000 Springer-Verlag.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
