Sciweavers

MEMOCODE
2006
IEEE

Mixed symbolic representations for model checking software programs

13 years 9 months ago
Mixed symbolic representations for model checking software programs
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 ordersof-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.
Zijiang Yang, Chao Wang, Aarti Gupta, Franjo Ivanc
Added 12 Jun 2010
Updated 12 Jun 2010
Type Conference
Year 2006
Where MEMOCODE
Authors Zijiang Yang, Chao Wang, Aarti Gupta, Franjo Ivancic
Comments (0)