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

Abstract

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
Pages831-836
Number of pages6
DOIs
StatePublished - Aug 25 2008
Externally publishedYes
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

Other

OtherDesign, Automation and Test in Europe, DATE 2008
CountryGermany
CityMunich
Period3/10/083/14/08

All Science Journal Classification (ASJC) codes

  • Engineering(all)

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

Cite this