NuSMV 2: An opensource tool for symbolic model checking

Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Enrico; Giunchiglia, Fausto; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando

doi:10.1007/3-540-45657-0_29

This paper describes version 2 of the NuSMV tool. NuSMV is a symbolic model checker originated from the reengineering, reimplementation and extension of SMV, the original BDD-based model checker developed at CMU. The NuSMV project aims at the development of a state-of-the-art symbolic model checker, designed to be applicable in technology transfer projects: it is a well structured, open, flexible and documented platform for model checking, and is robust and close to industrial systems standards.

NuSMV 2: An opensource tool for symbolic model checking / Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Enrico; Giunchiglia, Fausto; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando. - STAMPA. - 2404:(2002), pp. 359-364. (Intervento presentato al convegno CAV 2002 tenutosi a Copenhagen nel 27th July 2002) [10.1007/3-540-45657-0_29].

NuSMV 2: An opensource tool for symbolic model checking

Alessandro Cimatti;Edmund Clarke;Enrico Giunchiglia;Fausto Giunchiglia;Marco Pistore;Marco Roveri;Roberto Sebastiani;Armando Tacchella

2002-01-01

Abstract

This paper describes version 2 of the NuSMV tool. NuSMV is a symbolic model checker originated from the reengineering, reimplementation and extension of SMV, the original BDD-based model checker developed at CMU. The NuSMV project aims at the development of a state-of-the-art symbolic model checker, designed to be applicable in technology transfer projects: it is a well structured, open, flexible and documented platform for model checking, and is robust and close to industrial systems standards.

Scheda breve

Scheda completa

Scheda completa (DC)

	Anno di pubblicazione (Date of publication)
	
				2002
			
	Titolo del volume (Proceedings title)
	
				Computer Aided Verification. CAV 2002
			
	Luogo di edizione (Place of publication)
	
				Berlin, Heidelberg
			
	Casa editrice (Publisher)
	
				Springer
			
	ISBN
	
				978-3-540-43997-4
978-3-540-45657-5
			
	Codice Scopus (Scopus Identifier)
	
				2-s2.0-84937557946
			
	Tutti gli autori
	
						Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Enrico; Giunchiglia, Fausto; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando...espandi
						
	Citazione
	
				NuSMV 2: An opensource tool for symbolic model checking / Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Enrico; Giunchiglia, Fausto; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando. - STAMPA. - 2404:(2002), pp. 359-364. (Intervento presentato al  convegno CAV 2002 tenutosi a Copenhagen nel 27th July 2002) [10.1007/3-540-45657-0_29].
			
	Appare nelle tipologie:
	
				04.1 Saggio in atti di convegno (Paper in Proceedings)

File in questo prodotto:

File	Dimensione	Formato
cav02.pdf Solo gestori archivio Tipologia: Versione editoriale (Publisher’s layout) Licenza: Tutti i diritti riservati (All rights reserved) Dimensione 119.39 kB Formato Adobe PDF Visualizza/Apri	119.39 kB	Adobe PDF	Visualizza/Apri
file.pdf accesso aperto Tipologia: Post-print referato (Refereed author’s manuscript) Licenza: Tutti i diritti riservati (All rights reserved) Dimensione 91.43 kB Formato Adobe PDF Visualizza/Apri	91.43 kB	Adobe PDF	Visualizza/Apri