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

Abstract

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
Volume27
Issue number8
DOIs
StatePublished - Aug 2008

All Science Journal Classification (ASJC) codes

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

Keywords

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

Fingerprint

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

Cite this