Iterative Abstraction using SAT-Based BMC with Proof Analysis

Aarti Gupta, Malay Ganai, Zijiang Yang, Pranav Ashar

Research output: Contribution to journalConference articlepeer-review

63 Scopus citations


Resolution-based proof analysis techniques have been proposed recently to identify a sufficient set of reasons for unsatisfiability derived by a CNF-based SAT solver. We have adapted these techniques to work with a hybrid SAT solver. We use the proof analysis technique with SAT-based BMC, in order to generate useful abstract models. Our abstraction procedure is used iteratively in a top-down framework, starting from the concrete design, where we apply BMC on increasingly more abstract models. We apply various SAT-based and BDD-based verification methods on these abstract models, in order to obtain proofs of correctness, or to perform deeper searches for counterexamples. We demonstrate the effectiveness of our prototype implementation on several large industry designs.

Original languageEnglish (US)
Pages (from-to)416-423
Number of pages8
JournalIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers
StatePublished - 2003
EventIEEE/ACM International Conference on Computer Aided Design ICCAD 2003: IEEE/ACM Digest of Technical Papers - San Jose, CA, United States
Duration: Nov 9 2003Nov 13 2003

All Science Journal Classification (ASJC) codes

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


Dive into the research topics of 'Iterative Abstraction using SAT-Based BMC with Proof Analysis'. Together they form a unique fingerprint.

Cite this