Structure-Aware Computation of Predicate Abstraction

Reference:

Alessandro Cimatti, Jori Dubrovin, Tommi Junttila, and Marco Roveri. Structure-aware computation of predicate abstraction. In Armin Biere and Carl Pixley, editors, Proceedings of the 9th International Conference on Formal Methods in Computer Aided Design (FMCAD 2009), pages 9–16. IEEE, 2009.

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 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.

Suggested BibTeX entry:

@inproceedings{CimDubJunRov:FMCAD09,
    author = {Alessandro Cimatti and Jori Dubrovin and Tommi Junttila and Marco Roveri},
    booktitle = {Proceedings of the 9th International Conference on Formal Methods in Computer Aided Design (FMCAD 2009)},
    editor = {Armin Biere and Carl Pixley},
    pages = {9--16},
    publisher = {IEEE},
    title = {Structure-Aware Computation of Predicate Abstraction},
    year = {2009},
}

See dx.doi.org ...