Model checking automatically tests whether a model meets a given specification or not. It is a technique for verifying correctness properties of finite-state systems. One of the major problems in model checking is the state-explosion. To overcome this, a probabilistic approach called Bit-state Hashing is used to reduce the memory requirements. Bit-state hashing uses a data structure called bloom filter to store the corresponding reached states in a hash table. By enlarging a bloom filter, it improves total coverage estimation using a growth curve that approximates increased in reached states. To increase the effectiveness of the existing system, coverage estimation in model checking with sequential multiple bit-state hashing has been proposed. The sequentially repeated bit state hashing technique can outperform all other hashing methods, even for very large problem size.
Mutation Coverage Estimation for Model Checking
