학술논문

Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking
Document Type
Periodical
Source
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on. 27(8):1513-1517 Aug, 2008
Subject
Components, Circuits, Devices and Systems
Computing and Processing
Lab-on-a-chip
Explosions
Hardware
Data structures
Boolean functions
Context modeling
Upper bound
Application software
Software engineering
Data mining
Abstract interpretation
interval analysis
model checking
program analysis
software engineering
Language
ISSN
0278-0070
1937-4151
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.