@inproceedings{
    CimDubJunRov:FMCAD09,
    editor = "Biere, Armin and Pixley, Carl",
    author = "Cimatti, Alessandro and Dubrovin, Jori and Junttila, Tommi and Roveri, Marco",
    publisher = "IEEE",
    title = "Structure-Aware Computation of Predicate Abstraction",
    url = "http://dx.doi.org/10.1109/FMCAD.2009.5351149",
    booktitle = "Proceedings of the 9th International Conference on Formal Methods in Computer Aided Design (FMCAD 2009)",
    corerank = "NA",
    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.",
    opturl2 = "http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5351149",
    responsibleauthor = "Dubrovin, Jori",
    year = "2009",
    opturl = "http://ieeexplore.ieee.org/xpl/tocresult.jsp?isnumber=5351113&isYear=2009",
    impactfactor = "D3",
    pages = "9--16"
}