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.