The precise computation of abstractions is a bottleneck in many approaches to CEGAR-based verification. In this paper, we propose a novel approach, based on the use of structural information. Rather than computing the abstraction as a single, monolithic quantification, we provide a emph{structure-aware} abstraction algorithm, based on two complementary steps. The first, high-level step exploits the structure of the system, and partitions the abstraction problem into the combination of several smaller abstraction problems. This is represented as a formula with quantifiers. The second, low-level step exploits the structure of the formula, in particular the occurrence of variables within the quantifiers, and applies a set of low-level rewriting rules aiming at further reducing the scope of quantifiers. We experimentally evaluate the approach on a substantial set of benchmarks, and show significant speed ups compared to monolithic abstraction algorithms.

Structure-Aware Computation of Predicate Abstraction / Cimatti, Alessandro; Juhani Dubrovin, Jori; Antero Junttila, Tommi; Roveri, Marco. - (2009), pp. 9-16. (Intervento presentato al convegno FMCAD 2009 tenutosi a AUSTIN, TX, USA nel 15/11/2009 - 18/11/2009).

Structure-Aware Computation of Predicate Abstraction

Alessandro Cimatti;Marco Roveri
2009-01-01

Abstract

The precise computation of abstractions is a bottleneck in many approaches to CEGAR-based verification. In this paper, we propose a novel approach, based on the use of structural information. Rather than computing the abstraction as a single, monolithic quantification, we provide a emph{structure-aware} abstraction algorithm, based on two complementary steps. The first, high-level step exploits the structure of the system, and partitions the abstraction problem into the combination of several smaller abstraction problems. This is represented as a formula with quantifiers. The second, low-level step exploits the structure of the formula, in particular the occurrence of variables within the quantifiers, and applies a set of low-level rewriting rules aiming at further reducing the scope of quantifiers. We experimentally evaluate the approach on a substantial set of benchmarks, and show significant speed ups compared to monolithic abstraction algorithms.
2009
Proceedings of the Formal Methods in Computer Aided Design
AUSTIN, TX, USA
IEEE
9781424449668
Cimatti, Alessandro; Juhani Dubrovin, Jori; Antero Junttila, Tommi; Roveri, Marco
Structure-Aware Computation of Predicate Abstraction / Cimatti, Alessandro; Juhani Dubrovin, Jori; Antero Junttila, Tommi; Roveri, Marco. - (2009), pp. 9-16. (Intervento presentato al convegno FMCAD 2009 tenutosi a AUSTIN, TX, USA nel 15/11/2009 - 18/11/2009).
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/258769
 Attenzione

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

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