Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking

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...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on computer-aided design of integrated circuits and systems 2008-08, Vol.27 (8), p.1513-1517
Main Authors: Zaks, A., Zijiang Yang, Shlyakhter, I., Ivancic, F., Cadambi, S., Ganai, M.K., Gupta, A., Ashar, P.
Format: Article
Language:English
Subjects:
Abstract interpretation
Application software
Boolean functions
Computer programs
Context modeling
Data mining
Data structures
Design engineering
Explosions
Hardware
interval analysis
Intervals
Lab-on-a-chip
Mathematical analysis
Mathematical models
model checking
program analysis
Software
Software engineering
Upper bound
Weight reduction
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0278-0070
1937-4151
DOI:10.1109/TCAD.2008.925777