NUSMV: a new symbolic model checker

A. Cimatti¹ - E. Clarke² - F. Giunchiglia¹ - M. Roveri^1,3 - ¹ITC-IRST, Via Sommarive 18, 38055 Povo, Trento, Italy
{cimatti,fausto,roveri}@irst.itc.it
²SCS, Carnegie-Mellon University, 5000 Forbes Avenue, Pittsburgh, PA 15213-3891, USA
Edmund.Clarke@cs.cmu.edu
³DSI, University of Milano, Via Comelico 39, 20135 Milano, Italy

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.

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