Model checking sequential software programs via mixed symbolic analysis
Zijiang Yang, Chao Wang, Aarti Gupta, Franjo Ivančić · ACM Transactions on Design Automation of Electronic Systems · 2009
We present an efficient symbolic search algorithm for software model checking. Our algorithms perform word-level reasoning by using a combination of decision procedures in Boolean and integer and real domains, and use novel symbolic search strategies optimized specifically for sequential programs to improve scalability. Experiments on real-world C programs show that the new symbolic search algorithms can achieve several orders-of-magnitude improvements over existing methods based on bit-level (Boolean) reasoning.