Mixed symbolic representations for model checking software programs

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

Mixed symbolic representations for model checking software programs

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

17 Scopus citations

Abstract

We present an efficient symbolic search algorithm for software model checking. The algorithm combines multiple symbolic representations to efficiently represent the transition relation and reachable states and uses a combination of decision procedures for Boolean and integer representations. Our main contributions include: (1) mixed symbolic representations to model C programs with rich data types and complex expressions; and (2) new symbolic search strategies and optimization techniques specific to sequential programs that can significantly improve the scalability of model checking algorithms. Our controlled experiments on real-world software programs show that the new symbolic search algorithm can achieve several orders-of-magnitude improvements over existing methods. The proposed techniques are extremely competitive in handling sequential models of non-trivial sizes, and also compare favorably to popular Boolean-level model checking algorithms based on BDDs and SAT.

Original language	English (US)
Title of host publication	Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06
Pages	17-26
Number of pages	10
State	Published - 2006
Event	4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06 - Napa, CA, United States Duration: Jul 27 2006 → Jul 30 2006

Publication series

Name	Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06

Other

Other	4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06
Country/Territory	United States
City	Napa, CA
Period	7/27/06 → 7/30/06

All Science Journal Classification (ASJC) codes

Computer Networks and Communications
Hardware and Architecture
Software

Cite this

Yang, Z., Wang, C., Gupta, A., & Ivančić, F. (2006). Mixed symbolic representations for model checking software programs. In Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06 (pp. 17-26). Article 1695896 (Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06).

Yang, Zijiang ; Wang, Chao ; Gupta, Aarti et al. / Mixed symbolic representations for model checking software programs. Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06. 2006. pp. 17-26 (Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06).

@inproceedings{489bccb75fb341e19086dae68786f240,

title = "Mixed symbolic representations for model checking software programs",

abstract = "We present an efficient symbolic search algorithm for software model checking. The algorithm combines multiple symbolic representations to efficiently represent the transition relation and reachable states and uses a combination of decision procedures for Boolean and integer representations. Our main contributions include: (1) mixed symbolic representations to model C programs with rich data types and complex expressions; and (2) new symbolic search strategies and optimization techniques specific to sequential programs that can significantly improve the scalability of model checking algorithms. Our controlled experiments on real-world software programs show that the new symbolic search algorithm can achieve several orders-of-magnitude improvements over existing methods. The proposed techniques are extremely competitive in handling sequential models of non-trivial sizes, and also compare favorably to popular Boolean-level model checking algorithms based on BDDs and SAT.",

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

note = "Funding Information: A. Dargelas is supported by ANRT grant no 625/94; 4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06 ; Conference date: 27-07-2006 Through 30-07-2006",

year = "2006",

language = "English (US)",

isbn = "1424404215",

series = "Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06",

pages = "17--26",

booktitle = "Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06",

}

Yang, Z, Wang, C, Gupta, A & Ivančić, F 2006, Mixed symbolic representations for model checking software programs. in Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06., 1695896, Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06, pp. 17-26, 4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06, Napa, CA, United States, 7/27/06.

Mixed symbolic representations for model checking software programs. / Yang, Zijiang; Wang, Chao; Gupta, Aarti et al.
Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06. 2006. p. 17-26 1695896 (Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Mixed symbolic representations for model checking software programs

AU - Yang, Zijiang

AU - Wang, Chao

AU - Gupta, Aarti

AU - Ivančić, Franjo

N1 - Funding Information: A. Dargelas is supported by ANRT grant no 625/94

PY - 2006

Y1 - 2006

N2 - We present an efficient symbolic search algorithm for software model checking. The algorithm combines multiple symbolic representations to efficiently represent the transition relation and reachable states and uses a combination of decision procedures for Boolean and integer representations. Our main contributions include: (1) mixed symbolic representations to model C programs with rich data types and complex expressions; and (2) new symbolic search strategies and optimization techniques specific to sequential programs that can significantly improve the scalability of model checking algorithms. Our controlled experiments on real-world software programs show that the new symbolic search algorithm can achieve several orders-of-magnitude improvements over existing methods. The proposed techniques are extremely competitive in handling sequential models of non-trivial sizes, and also compare favorably to popular Boolean-level model checking algorithms based on BDDs and SAT.

AB - We present an efficient symbolic search algorithm for software model checking. The algorithm combines multiple symbolic representations to efficiently represent the transition relation and reachable states and uses a combination of decision procedures for Boolean and integer representations. Our main contributions include: (1) mixed symbolic representations to model C programs with rich data types and complex expressions; and (2) new symbolic search strategies and optimization techniques specific to sequential programs that can significantly improve the scalability of model checking algorithms. Our controlled experiments on real-world software programs show that the new symbolic search algorithm can achieve several orders-of-magnitude improvements over existing methods. The proposed techniques are extremely competitive in handling sequential models of non-trivial sizes, and also compare favorably to popular Boolean-level model checking algorithms based on BDDs and SAT.

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

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

M3 - Conference contribution

AN - SCOPUS:38149023941

SN - 1424404215

SN - 9781424404216

T3 - Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06

SP - 17

EP - 26

BT - Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06

T2 - 4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06

Y2 - 27 July 2006 through 30 July 2006

ER -

Mixed symbolic representations for model checking software programs

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Other files and links

Fingerprint

Cite this