Completeness in SMT-based BMC for software programs

Malay K. Ganai, Aarti Gupta

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

13 Scopus citations


Bounded Model Checking (BMC) is incomplete without a completeness threshold (CT ) bound. Previous methods, using recurrence diameter for obtaining CT , check for existence of a longest loop-free path at every depth k. For terminating software programs, we propose an efficient method for obtaining CT that requires solving a formula of size O(k) at some depths only, as compared to previous methods that require solving a formula of O(k2) (or O(klogk)) size at every depth. We augment previous methods for BMC simplifications using model transformation and control flow information, with context-sensitive analysis. This results in more BMC simplifications and further reduction in the number of CT checks. We have implemented our techniques in a Satisfiability Modulo Theory (SMT)-based BMC framework. Our controlled experiments on real-world software programs show that our proposed formulation provides significant improvements over previous approaches.

Original languageEnglish (US)
Title of host publicationDesign, Automation and Test in Europe, DATE 2008
Number of pages6
StatePublished - 2008
EventDesign, Automation and Test in Europe, DATE 2008 - Munich, Germany
Duration: Mar 10 2008Mar 14 2008

Publication series

NameProceedings -Design, Automation and Test in Europe, DATE
ISSN (Print)1530-1591


OtherDesign, Automation and Test in Europe, DATE 2008

All Science Journal Classification (ASJC) codes

  • General Engineering


Dive into the research topics of 'Completeness in SMT-based BMC for software programs'. Together they form a unique fingerprint.

Cite this