loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
15th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ecbs 2008)
Counterexample Guided Abstraction Refinement is Better under Equational Abstraction
March 31-April 04
ISBN: 978-0-7695-3141-0
ASCII Text
x 
 
Constantin Enea, "Counterexample Guided Abstraction Refinement is Better under Equational Abstraction," Engineering of Computer-Based Systems, IEEE International Conference on the, pp. 126-135, 15th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ecbs 2008), 2008.
 
 
BibTex
x
 
@article{ 10.1109/ECBS.2008.40,
author = {Constantin Enea},
title = {Counterexample Guided Abstraction Refinement is Better under Equational Abstraction},
journal ={Engineering of Computer-Based Systems, IEEE International Conference on the},
volume = {0},
year = {2008},
isbn = {978-0-7695-3141-0},
pages = {126-135},
doi = {http://doi.ieeecomputersociety.org/10.1109/ECBS.2008.40},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Engineering of Computer-Based Systems, IEEE International Conference on the
TI - Counterexample Guided Abstraction Refinement is Better under Equational Abstraction
SN - 978-0-7695-3141-0
SP126
EP135
A1 - Constantin Enea,
PY - 2008
KW - verification
KW - equational abstraction
KW - refinement
KW - CEGAR
VL - 0
JA - Engineering of Computer-Based Systems, IEEE International Conference on the
ER -
 
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.
Index Terms:
verification, equational abstraction, refinement, CEGAR
Citation:
Constantin Enea, "Counterexample Guided Abstraction Refinement is Better under Equational Abstraction," ecbs, pp.126-135, 15th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ecbs 2008), 2008
Usage of this product signifies your acceptance of the Terms of Use.