Symbolic model checking is a very successful formal verification technique, classically based on Binary Decision Diagrams (BDDs). Recently, propositional satisfiability (SAT) techniques have been proposed as a computational basis for symbolic model checking, and proved to be an effective alternative to BDD-based techniques. In this paper we show how BDD-based and SAT-based techniques have been effectively integrated within the NuSMV symbolic model checker.

Integrating BDD-based and SAT-based Symbolic Model Checking / Cimatti, Alessandro; Giunchiglia, Enrico; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando; Pistore, Marco. - ELETTRONICO. - (2002).

Integrating BDD-based and SAT-based Symbolic Model Checking

Cimatti, Alessandro;Roveri, Marco;Sebastiani, Roberto;Pistore, Marco
2002-01-01

Abstract

Symbolic model checking is a very successful formal verification technique, classically based on Binary Decision Diagrams (BDDs). Recently, propositional satisfiability (SAT) techniques have been proposed as a computational basis for symbolic model checking, and proved to be an effective alternative to BDD-based techniques. In this paper we show how BDD-based and SAT-based techniques have been effectively integrated within the NuSMV symbolic model checker.
2002
Trento, Italia
Università degli Studi di Trento. DEPARTMENT OF INFORMATION AND COMMUNICATION TECHNOLOGY
Integrating BDD-based and SAT-based Symbolic Model Checking / Cimatti, Alessandro; Giunchiglia, Enrico; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando; Pistore, Marco. - ELETTRONICO. - (2002).
Cimatti, Alessandro; Giunchiglia, Enrico; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando; Pistore, Marco
File in questo prodotto:
File Dimensione Formato  
45.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 193.68 kB
Formato Adobe PDF
193.68 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/358375
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact