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 -