State-Space Coverage Estimation

Software model checking is the process of systematically exploring a program's state space to find hard-to-discover errors. Because of the exponential size of the state space, an exhaustive search of the state space is often impossible given the memory resources. In such cases, an estimate of how much of the state space is covered can help the verifier to decide whether to employ additional computational resources or to use more aggressive abstraction techniques. Our work focuses on coverage estimation for explicit-state model checking of software programs. In this paper, we present an estimation algorithm that is based on Monte Carlo techniques that sample the unexplored portion of the reachability graph. We implemented our algorithm in Java Pathfinder and evaluated our approach on a suite of Java programs, simulating out-of-memory errors after a known percentage of a program's state space had been searched. Our empirical studies show that, on average, our algorithm's coverage estimates differ from the actual coverage by less than 10 percentage points, with a standard deviation of about 5 percentage points - regardless of whether the actual state-space coverage is low (3%) or high (95%).