Sciweavers

Share
ICCAD
2007
IEEE

Hybrid CEGAR: combining variable hiding and predicate abstraction

10 years 15 days ago
Hybrid CEGAR: combining variable hiding and predicate abstraction
ion Chao Wang NEC Laboratories America Hyondeuk Kim University of Colorado Aarti Gupta NEC Laboratories America Variable hiding and predicate abstraction are two popular abstraction methods to obtain simplified 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 refinement (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 refinement based on weakest preconditions to add new predicates, and under certain conditions trade in the predicates for visible variables bstract 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 find more effective unsatisfiable cores for refinement. We have implemented the proposed hybrid CEGAR pro...
Chao Wang, Hyondeuk Kim, Aarti Gupta
Added 16 Mar 2010
Updated 16 Mar 2010
Type Conference
Year 2007
Where ICCAD
Authors Chao Wang, Hyondeuk Kim, Aarti Gupta
Comments (0)
books