Bitwidth reduction via symbolic interval analysis for software model checking

Aleksandr Zaks; Zijiang Yang; Ilya Shlyakhter; Franjo Ivančić; Srihari Cadambi; Malay K. Ganai; Aarti Gupta; Pranav Ashar

doi:10.1109/TCAD.2008.925777

Bitwidth reduction via symbolic interval analysis for software model checking

Aleksandr Zaks
, Zijiang Yang
, Ilya Shlyakhter
, Franjo Ivančić
, Srihari Cadambi
, Malay K. Ganai
, Aarti Gupta
, Pranav Ashar

电子与信息学部

Alphabet Inc.
Broad Institute
NEC Corporation

科研成果: 期刊稿件 › 文章 › 同行评审

12 引用（Scopus）

摘要

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.

源语言	英语
文章编号	4527113
页（从-至）	1513-1517
页数	5
期刊	IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
卷	27
期	8
DOI	https://doi.org/10.1109/TCAD.2008.925777
出版状态	已出版 - 8月 2008

访问文件

10.1109/TCAD.2008.925777

其它文件与链接

链接到 Scopus 的出版物

引用此

@article{7ea30cf951b34eb6a1392e90dfe9452c,

title = "Bitwidth reduction via symbolic interval analysis for software model checking",

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 = "Abstract interpretation, Interval analysis, Model checking, Program analysis, Software engineering",

author = "Aleksandr Zaks and Zijiang Yang and Ilya Shlyakhter and Franjo Ivan{\v c}i{\'c} and Srihari Cadambi and Ganai, \{Malay K.\} and Aarti Gupta and Pranav Ashar",

year = "2008",

month = aug,

doi = "10.1109/TCAD.2008.925777",

language = "英语",

volume = "27",

pages = "1513--1517",

journal = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems",

issn = "0278-0070",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

number = "8",

}

TY - JOUR

T1 - Bitwidth reduction via symbolic interval analysis for software model checking

AU - Zaks, Aleksandr

AU - Yang, Zijiang

AU - Shlyakhter, Ilya

AU - Ivančić, Franjo

AU - Cadambi, Srihari

AU - Ganai, Malay K.

AU - Gupta, Aarti

AU - Ashar, Pranav

PY - 2008/8

Y1 - 2008/8

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

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

KW - Abstract interpretation

KW - Interval analysis

KW - Model checking

KW - Program analysis

KW - Software engineering

UR - https://www.scopus.com/pages/publications/47849109477

U2 - 10.1109/TCAD.2008.925777

DO - 10.1109/TCAD.2008.925777

M3 - 文章

AN - SCOPUS:47849109477

SN - 0278-0070

VL - 27

SP - 1513

EP - 1517

JO - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

JF - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

IS - 8

M1 - 4527113

ER -

Bitwidth reduction via symbolic interval analysis for software model checking

摘要

访问文件

其它文件与链接

学术指纹

引用此