Model checking sequential software programs via mixed symbolic analysis

Zijiang Yang; Chao Wang; Aarti Gupta; Franjo Ivanĉić

doi:10.1145/1455229.1455239

Model checking sequential software programs via mixed symbolic analysis

Zijiang Yang, Chao Wang, Aarti Gupta, Franjo Ivanĉić

Computer Science

Research output: Contribution to journal › Article › peer-review

11 Scopus citations

Abstract

We present an efficient symbolic search algorithm for software model checking. Our algorithms perform word-level reasoning by using a combination of decision procedures in Boolean and integer and real domains, and use novel symbolic search strategies optimized specifically for sequential programs to improve scalability. Experiments on real-world C programs show that the new symbolic search algorithms can achieve several orders-of-magnitude improvements over existing methods based on bit-level (Boolean) reasoning.

Original language	English (US)
Article number	10
Journal	ACM Transactions on Design Automation of Electronic Systems
Volume	14
Issue number	1
DOIs	https://doi.org/10.1145/1455229.1455239
State	Published - Jan 1 2009

All Science Journal Classification (ASJC) codes

Computer Science Applications
Computer Graphics and Computer-Aided Design
Electrical and Electronic Engineering

Keywords

Binary decision diagram
Composite symbolic formula
Image computation
Model checking
Presburger arithmetic
Reachability analysis

Access to Document

10.1145/1455229.1455239

Cite this

@article{bc555d612abe414087202b95da5d80cc,

title = "Model checking sequential software programs via mixed symbolic analysis",

abstract = "We present an efficient symbolic search algorithm for software model checking. Our algorithms perform word-level reasoning by using a combination of decision procedures in Boolean and integer and real domains, and use novel symbolic search strategies optimized specifically for sequential programs to improve scalability. Experiments on real-world C programs show that the new symbolic search algorithms can achieve several orders-of-magnitude improvements over existing methods based on bit-level (Boolean) reasoning.",

keywords = "Binary decision diagram, Composite symbolic formula, Image computation, Model checking, Presburger arithmetic, Reachability analysis",

author = "Zijiang Yang and Chao Wang and Aarti Gupta and Franjo Ivanĉi{\'c}",

year = "2009",

month = jan,

day = "1",

doi = "10.1145/1455229.1455239",

language = "English (US)",

volume = "14",

journal = "ACM Transactions on Design Automation of Electronic Systems",

issn = "1084-4309",

publisher = "Association for Computing Machinery (ACM)",

number = "1",

}

TY - JOUR

T1 - Model checking sequential software programs via mixed symbolic analysis

AU - Yang, Zijiang

AU - Wang, Chao

AU - Gupta, Aarti

AU - Ivanĉić, Franjo

PY - 2009/1/1

Y1 - 2009/1/1

N2 - We present an efficient symbolic search algorithm for software model checking. Our algorithms perform word-level reasoning by using a combination of decision procedures in Boolean and integer and real domains, and use novel symbolic search strategies optimized specifically for sequential programs to improve scalability. Experiments on real-world C programs show that the new symbolic search algorithms can achieve several orders-of-magnitude improvements over existing methods based on bit-level (Boolean) reasoning.

AB - We present an efficient symbolic search algorithm for software model checking. Our algorithms perform word-level reasoning by using a combination of decision procedures in Boolean and integer and real domains, and use novel symbolic search strategies optimized specifically for sequential programs to improve scalability. Experiments on real-world C programs show that the new symbolic search algorithms can achieve several orders-of-magnitude improvements over existing methods based on bit-level (Boolean) reasoning.

KW - Binary decision diagram

KW - Composite symbolic formula

KW - Image computation

KW - Model checking

KW - Presburger arithmetic

KW - Reachability analysis

UR - http://www.scopus.com/inward/record.url?scp=60349086094&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=60349086094&partnerID=8YFLogxK

U2 - 10.1145/1455229.1455239

DO - 10.1145/1455229.1455239

M3 - Article

AN - SCOPUS:60349086094

SN - 1084-4309

VL - 14

JO - ACM Transactions on Design Automation of Electronic Systems

JF - ACM Transactions on Design Automation of Electronic Systems

IS - 1

M1 - 10

ER -

Model checking sequential software programs via mixed symbolic analysis

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this