Sciweavers

Share
ICCAD
2010
IEEE

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

10 years 9 months ago
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...
Malay K. Ganai, Chao Wang, Weihong Li
Added 11 Feb 2011
Updated 11 Feb 2011
Type Journal
Year 2010
Where ICCAD
Authors Malay K. Ganai, Chao Wang, Weihong Li
Comments (0)
books