Efficient SAT-based bounded model checking for software verification

Franjo Ivančić, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Pranav Ashar

Research output: Contribution to journalArticlepeer-review

63 Scopus citations


This paper discusses our methodology for formal analysis and automatic verification of software programs. It is applicable to a large subset of the C programming language that includes pointer arithmetic and bounded recursion. We consider reachability properties, in particular whether certain assertions or basic blocks are reachable in the source code, or whether certain standard property violations can occur. We perform this analysis via a translation to a Boolean circuit representation based on modeling basic blocks. The program is then analyzed by a back-end SAT-based bounded model checker, where each unrolling is mapped to one step in a block-wise execution of the program. The main contributions of this paper are as follows: (1) Use of basic block-based unrollings with SAT-based bounded model checking of software programs. This allows us to take advantage of SAT-based learning inherent to the best performing bounded model checkers. (2) Various heuristics customized for models automatically generated from software, allowing a more efficient SAT-based analysis. (3) A prototype tool called F-Soft has been implemented using our methodology. We present experimental results based on multiple case studies including a C-based implementation of a network protocol, and compare the performance gains using the proposed heuristics.

Original languageEnglish (US)
Pages (from-to)256-274
Number of pages19
JournalTheoretical Computer Science
Issue number3
StatePublished - Sep 28 2008

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


  • Bounded model checking
  • SAT-based model checking
  • Software verification


Dive into the research topics of 'Efficient SAT-based bounded model checking for software verification'. Together they form a unique fingerprint.

Cite this