TY - GEN
T1 - Counterexample guided abstraction refinement is better under equational abstraction
AU - Enea, Constantin
PY - 2008/5/28
Y1 - 2008/5/28
N2 - We introduce an improved version of the equational abstraction for rewrite theories in which the temporal logic used handles also maximal finite paths and the representation of the atomic propositions, by itself, can not lead to useless abstractions. Afterward, we establish a counterexample guided abstraction refinement procedure under equational abstraction and we prove by a consistent example that it may lead to better abstractions than in the case of the classical counterexample guided abstraction refinement procedure under predicate abstraction. The new procedure offers us for free something similar to the localization for predicate abstraction and it is able to reuse the already developed heuristics for discovering predicates that eliminate spurious counterexamples.
AB - We introduce an improved version of the equational abstraction for rewrite theories in which the temporal logic used handles also maximal finite paths and the representation of the atomic propositions, by itself, can not lead to useless abstractions. Afterward, we establish a counterexample guided abstraction refinement procedure under equational abstraction and we prove by a consistent example that it may lead to better abstractions than in the case of the classical counterexample guided abstraction refinement procedure under predicate abstraction. The new procedure offers us for free something similar to the localization for predicate abstraction and it is able to reuse the already developed heuristics for discovering predicates that eliminate spurious counterexamples.
UR - https://www.scopus.com/pages/publications/44149104640
U2 - 10.1109/ECBS.2008.40
DO - 10.1109/ECBS.2008.40
M3 - Conference contribution
AN - SCOPUS:44149104640
SN - 0769531415
SN - 9780769531410
T3 - Proceedings - Fifteenth IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, ECBS 2008
SP - 126
EP - 135
BT - Proceedings - Fifteenth IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, ECBS 2008
T2 - 15th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, ECBS 2008
Y2 - 31 March 2008 through 4 April 2008
ER -