Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking
Aleksandr Zaks, Zijiang Yang, Ilya A. Shlyakhter, Franjo Ivančić, Srihari Cadambi, Malay Ganai, Aarti Gupta, Pranav N Ashar · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · 2008
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.