Trading off SAT Search and Variable Quantifications for Effective Unbounded Model Checking

Tipo di pubblicazione: Articolo in atti di convegno
Tipologia MIUR: Contributo in Atti di Convegno (Proceeding) > Contributo in atti di convegno
Titolo: Trading off SAT Search and Variable Quantifications for Effective Unbounded Model Checking
Autori: Cabodi G.; P. Camurati; M. Murciano; L. Garcia; S. Nocco; S. Quer
Autori di ateneo:
Intervallo pagine: pp. 205-212
Editore: IEEE
ISBN: 9781424427352
Titolo del convegno: FMCAD 2008: Formal Methods in Computer Aided Design
Luogo dell'evento: Portland, OR, USA
Data dell'evento: 17-20 novembre 2008
Rilevanza dell'evento: Internazionale
Luogo di pubblicazione: NEW YORK, NY
Abstract: Interpolant-based model checking has been shown effective on large verification instances, as it efficiently combines automated abstraction and fixed-point checks. On the other hand, methods based on variable quantification have proved their ability to remove free inputs, thus projecting the search space over state variables. In this paper we propose an integrated approach combining the abstraction power of interpolation with techniques relying on AIG and/or BDD representations of states, supporting variable quantification and fixed-point checks. The underlying idea of this combination is to adopt AIG- or BDD-based quantifications to limit and restrict the search space (and the complexity) of the interpolant-based approach. The exploited strategies, individually well-known, are integrated with a new flavor, specifically designed to improve their effectiveness on large verification instances. Experimental results, oriented to hard-to-solve verification problems, show the robustness of our approach
Data: 2008
Status: Pubblicato
Lingua della pubblicazione: Inglese
Parole chiave: model-checking, sat proof
Dipartimenti (originale): DAUIN - Dipartimento di Automatica Informatica
Dipartimenti: DAUIN - Dipartimento di Automatica e Informatica
URL correlate:
    Area disciplinare: Area 09 - Ingegneria industriale e dell'informazione > SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
    Data di deposito: 15 Ott 2008 12:13
    Data ultima modifica (IRIS): 20 Ott 2016 11:53:33
    Data inserimento (PORTO): 22 Ott 2016 04:39
    Permalink: http://porto.polito.it/id/eprint/1847472
    Link resolver URL: Link resolver link
    Citazioni:

    Il campo presenta il numero di citazioni presenti sulle banche dati Scopus e Web of Science e permette di accedere ai relativi record. Visualizza inoltre il link al record presente su Google Scholar.

    Possono verificarsi discrepanze rispetto ai dati presenti sulle banche dati per i seguenti motivi:

    • Differenze tra i dati riportati su IRIS e quelli presenti nelle banche dati.
    • Il numero di citazioni riportate su PORTO viene estratto mensilmente. Il dato citazionale presente sulle singole banche dati è aggiornato in tempo reale
    • Il numero di citazioni per WoS viene calcolato sulla base delle collezioni in abbonamento (Science citation index Expanded e Conference Proceedings Citation Index)

    Per informazioni o segnalazioni contattare scrivia/porto

    +
    -

    Allegati

    [img] PDF (FMCAD2008.pdf) - Postprint
    Accesso al documento: Non visibile (accessibile solo al proprietario del dato)
    Licenza: Non pubblico - Accesso privato / Ristretto.

    Download (167Kb (171057 bytes)) | Spedisci una richiesta all'autore per una copia del documento

    Azioni (richiesto il login)

    Visualizza il documento (riservato amministratori) Visualizza il documento (riservato amministratori)