next up previous
Next: Introduction Up: NuSMV papers

NUSMV: a new symbolic model checker

A. Cimatti1 - E. Clarke2 - F. Giunchiglia1 - M. Roveri1,3 - 1ITC-IRST, Via Sommarive 18, 38055 Povo, Trento, Italy
2SCS, Carnegie-Mellon University, 5000 Forbes Avenue, Pittsburgh, PA 15213-3891, USA
3DSI, University of Milano, Via Comelico 39, 20135 Milano, Italy


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.

Key words Symbolic Model Checking - Temporal Logics - Automatic verification - Tools for technology transfer.


NuSMV < >