@inproceedings{2c761019d5fc4724a47365a07afe1142,
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}",
year = "2006",
language = "英语",
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",
note = "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",
}