Hybrid CEGAR: Combining variable hiding and predicate abstraction

Chao Wang, Hyondeuk Kim, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publication2007 IEEE/ACM International Conference on Computer-Aided Design, ICCAD
Pages310-317
Number of pages8
DOIs
StatePublished - Dec 1 2007
Externally publishedYes
Event2007 IEEE/ACM International Conference on Computer-Aided Design, ICCAD - San Jose, CA, United States
Duration: Nov 4 2007Nov 8 2007

Publication series

NameIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
ISSN (Print)1092-3152

Other

Other2007 IEEE/ACM International Conference on Computer-Aided Design, ICCAD
CountryUnited States
CitySan Jose, CA
Period11/4/0711/8/07

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Hybrid CEGAR: Combining variable hiding and predicate abstraction'. Together they form a unique fingerprint.

Cite this