TY - GEN
T1 - Hybrid CEGAR
T2 - 2007 IEEE/ACM International Conference on Computer-Aided Design, ICCAD
AU - Wang, Chao
AU - Kim, Hyondeuk
AU - Gupta, Aarti
PY - 2007
Y1 - 2007
N2 - Variable hiding and predicate abstraction are two popular abstraction methods to obtain simpli ed models for model checking. Although both methods have been used successfully in practice, no attempt has been made to combine them in counterexample guided abstraction re nement (CEGAR). In this paper, we propose a hybrid abstraction method that allows both visible variables and predicates to take advantages of their relative strengths. We use re nement based on weakest preconditions to add new predicates, and under certain conditions trade in the predicates for visible variables in the abstract model. We also present heuristics for improving the overall performance, based on static analysis to identify useful candidates for visible variables, and use of lazy constraints to nd more effective unsatis able cores for re nement. We have implemented the proposed hybrid CEGAR procedure. Our experiments on public benchmarks show that the new abstraction method frequently outperforms the better of the two existing abstraction methods.
AB - Variable hiding and predicate abstraction are two popular abstraction methods to obtain simpli ed models for model checking. Although both methods have been used successfully in practice, no attempt has been made to combine them in counterexample guided abstraction re nement (CEGAR). In this paper, we propose a hybrid abstraction method that allows both visible variables and predicates to take advantages of their relative strengths. We use re nement based on weakest preconditions to add new predicates, and under certain conditions trade in the predicates for visible variables in the abstract model. We also present heuristics for improving the overall performance, based on static analysis to identify useful candidates for visible variables, and use of lazy constraints to nd more effective unsatis able cores for re nement. We have implemented the proposed hybrid CEGAR procedure. Our experiments on public benchmarks show that the new abstraction method frequently outperforms the better of the two existing abstraction methods.
UR - http://www.scopus.com/inward/record.url?scp=50249182145&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=50249182145&partnerID=8YFLogxK
U2 - 10.1109/ICCAD.2007.4397283
DO - 10.1109/ICCAD.2007.4397283
M3 - Conference contribution
AN - SCOPUS:50249182145
SN - 1424413826
SN - 9781424413829
T3 - IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
SP - 310
EP - 317
BT - 2007 IEEE/ACM International Conference on Computer-Aided Design, ICCAD
Y2 - 4 November 2007 through 8 November 2007
ER -