In this paper, we introduce a model-checking-based certification technique called search-carrying code (SCC). SCC is an adaptation of the principles of proof-carrying code, in which program certification is reduced to checking a provided safety proof. In SCC, program certification is an efficient re-examination of a program's state space. A code producer, who offers a program for use, provides a search script that encodes a search of the program's state space. A code consumer, who wants to certify that the program fits her needs, uses the search script to direct how a model checker searches the program's state space.

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%).