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...

• Type: Conference
• Year: 2007
• Where: ICCAD
• Authors: Chao Wang, Hyondeuk Kim, Aarti Gupta
• Keywords: Counterexample Guided Abstraction, Hardware, Hybrid Abstraction Method, ICCAD 2007, Popular Abstraction Methods