Bitwidth reduction via symbolic interval analysis for software model checking

Aleksandr Zaks, Zijiang Yang, Ilya Shlyakhter, Franjo Ivančić, Srihari Cadambi, Malay K. Ganai, Aarti Gupta, Pranav Ashar

Research output: Contribution to journalArticlepeer-review

12 Scopus citations


This paper presents a lightweight interval analysis technique for determining the lower and upper bounds for program variables and its application in improving software model checking techniques. The experiments demonstrate that it is an effective approach to alleviate the state explosion problem in software model checking.

Original languageEnglish (US)
Article number4527113
Pages (from-to)1513-1517
Number of pages5
JournalIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Issue number8
StatePublished - Aug 2008

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering


  • Abstract interpretation
  • Interval analysis
  • Model checking
  • Program analysis
  • Software engineering


Dive into the research topics of 'Bitwidth reduction via symbolic interval analysis for software model checking'. Together they form a unique fingerprint.

Cite this