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
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;
Journal_Title :
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
DOI :
10.1109/TCAD.2008.925777
