Abstract Model Checking without Computing the Abstraction Export

@incollection{citeulike:6082920, abstract = {Abstraction is a fundamental technique that enables the verification of large systems. In symbolic model checking, abstractions are defined by formulas that relate concrete and abstract variables. In predicate abstraction, the abstract variables are equivalent to some predicates over the concrete variables. In order to apply model checking on the abstract state space, it is usually necessary to compute a quantifier-free formula that is equivalent to the abstract transition relation. In predicate abstraction, the quantifier elimination can be obtained by solving an ALLSAT problem. In many practical cases, this computation results into a bottleneck. In this paper, we propose a new algorithm that combines abstraction with bounded model checking and k-induction. The algorithm does not rely on quantifier elimination, but encodes the model checking problem over the abstract state space into SAT problems. The algorithm is a novelty in the state-of-the-art of abstract model checking because it avoids computing the abstraction. An experimental evaluation with case studies taken from an industrial project shows that the new algorithm is more efficient and reaches in some cases a time improvement that is exponential in the number of predicates.}, author = {Tonetta, Stefano}, citeulike-article-id = {6082920}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-05089-3_7}, citeulike-linkout-1 = {http://www.springerlink.com/content/f71r341t34hg3747}, doi = {10.1007/978-3-642-05089-3_7}, journal = {FM 2009: Formal Methods}, keywords = {2009, fundamental\_technique, model\_checking, quantifier\_elimination, state\_of\_the\_art, symbolic\_model\_checking}, pages = {89--105}, posted-at = {2009-11-07 13:42:02}, priority = {4}, title = {Abstract Model Checking without Computing the Abstraction}, url = {http://dx.doi.org/10.1007/978-3-642-05089-3_7}, year = {2009} }

TY - CHAP ID - citeulike:6082920 L3 - citeulike-article-id:6082920 N2 - Abstraction is a fundamental technique that enables the verification of large systems. In symbolic model checking, abstractions are defined by formulas that relate concrete and abstract variables. In predicate abstraction, the abstract variables are equivalent to some predicates over the concrete variables. In order to apply model checking on the abstract state space, it is usually necessary to compute a quantifier-free formula that is equivalent to the abstract transition relation. In predicate abstraction, the quantifier elimination can be obtained by solving an ALLSAT problem. In many practical cases, this computation results into a bottleneck. In this paper, we propose a new algorithm that combines abstraction with bounded model checking and k-induction. The algorithm does not rely on quantifier elimination, but encodes the model checking problem over the abstract state space into SAT problems. The algorithm is a novelty in the state-of-the-art of abstract model checking because it avoids computing the abstraction. An experimental evaluation with case studies taken from an industrial project shows that the new algorithm is more efficient and reaches in some cases a time improvement that is exponential in the number of predicates. JF - FM 2009: Formal Methods EP - 105 TI - Abstract Model Checking without Computing the Abstraction SP - 89 KW - 2009 KW - fundamental_technique KW - model_checking KW - quantifier_elimination KW - state_of_the_art KW - symbolic_model_checking AU - Tonetta, Stefano PY - 2009/// UR - http://dx.doi.org/10.1007/978-3-642-05089-3_7 ER -