• DocumentCode
    1229339
  • Title

    Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking

  • Author

    Zaks, Aleksandr ; Yang, Zijiang ; Shlyakhter, Ilya ; Ivancic, Franjo ; Cadambi, Srihari ; Ganai, Malay K. ; Gupta, Aarti ; Ashar, Pranav

  • Author_Institution
    Google, Mountain View, CA
  • Volume
    27
  • Issue
    8
  • fYear
    2008
  • Firstpage
    1513
  • Lastpage
    1517
  • 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.
  • Keywords
    program diagnostics; program verification; bitwidth reduction; lower bound; program variables; software model checking; state explosion problem; symbolic interval analysis; upper bound; Abstract interpretation; interval analysis; model checking; program analysis; software engineering;
  • fLanguage
    English
  • Journal_Title
    Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
  • Publisher
    ieee
  • ISSN
    0278-0070
  • Type

    jour

  • DOI
    10.1109/TCAD.2008.925777
  • Filename
    4527113
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1229339