Counterexample Guided Abstraction Refinement is Better under Equational Abstraction

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.