Tunneling and slicing: Towards scalable BMC

Malay Ganai, Aarti Gupta

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

16 Scopus citations


Bounded Model Checking (BMC) provides complete design coverage with respect to a correctness property up to a bounded depth. However, with successive unrolling of the design, each BMC instance at depth k becomes bigger in size and harder to solve. We propose a novel scalable approach to decompose disjunctively a BMC instance, into simpler and independent subproblems, based on tunnels i.e., a set of control paths. We simplify each subproblem using slicing, data path simplification and tunnel specific control flow constraints, and solve them independently. We implemented such a tunneling and slicing-based reduction (TSR) approach in Satisfiability-Modulo-Theory (SMT)-based BMC framework. Such a TSR-based approach improves the overall performance of BMC when applied to verification of lowlevel embedded industry programs.

Original languageEnglish (US)
Title of host publicationProceedings of the 45th Design Automation Conference, DAC
Number of pages6
StatePublished - 2008
Event45th Design Automation Conference, DAC - Anaheim, CA, United States
Duration: Jun 8 2008Jun 13 2008

Publication series

NameProceedings - Design Automation Conference
ISSN (Print)0738-100X


Other45th Design Automation Conference, DAC
Country/TerritoryUnited States
CityAnaheim, CA

All Science Journal Classification (ASJC) codes

  • Control and Systems Engineering
  • Hardware and Architecture


  • BMC
  • CFG
  • CSR
  • EFSM
  • Partitioning
  • SMT
  • Slice
  • Tunnel


Dive into the research topics of 'Tunneling and slicing: Towards scalable BMC'. Together they form a unique fingerprint.

Cite this