Mixed symbolic representations for model checking software programs

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

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationProceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06
Pages17-26
Number of pages10
StatePublished - Dec 1 2006
Externally publishedYes
Event4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06 - Napa, CA, United States
Duration: Jul 27 2006Jul 30 2006

Publication series

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

Other

Other4th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06
CountryUnited States
CityNapa, CA
Period7/27/067/30/06

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Hardware and Architecture
  • Software

Fingerprint Dive into the research topics of 'Mixed symbolic representations for model checking software programs'. Together they form a unique fingerprint.

  • 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). [1695896] (Proceedings - Fourth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'06).