Efficient state space exploration: Interleaving stateless and state-based model checking

State-based model checking methods comprise computing and storing reachable states, while stateless model checking methods directly reason about reachable paths using decision procedures, thereby avoiding computing and storing the reachable states. Typically, statebased methods involve memory-intensive operations, while stateless methods involve time-intensive operations. We propose a divide-andconquer strategy to combine the complementary strengths of these methods for efficient verification of embedded software. Specifically, our model checking engine uses both state decomposition and state prioritization to guide the combination of a Presburger arithmetic based symbolic traversal algorithm (state-based) and an SMT based bounded model checking algorithm (stateless). These two underlying algorithms are interleaved--based on memory/time bounds and dynamic task partitioning--in order to systematically explore the state space and to avoid storing the entire reachable state set. We have i...

• Type: Journal
• Year: 2010
• Where: ICCAD
• Authors: Malay K. Ganai, Chao Wang, Weihong Li
• Keywords: Checking, Hardware, ICCAD 2010, Model, Reachable State