The most interesting model checking technique (from the assigned papers) is, in my opinion, stateless search.

Stateless search is a technique that enables model checkers, such as VeriSoft, to explore large state spaces without maintaining states in memory. Thus, stateless search completely eliminates the need to maintain a state-space cache. Instead, it performs deterministic executions of concurrent programs by automatically controlling the execution of synchronization operations. The main limitation of stateless search is redundant exploration, which is addressed by an optimization, called partial order reduction. Partial order reduction avoids exploring totally-ordered interleavings that have the same partial order. In a nutshell, the partial order reduction optimization typically performs a static analysis of the code to infer which thread interleavings commute, and avoids exploring all but one of these interleavings

Stateless search is a clever technique, that partially solves an important problem: model checkers were not able to explore large state-spaces due to memory consumption. Thus, before the advent of VeriSoftʼs stateless search technique, model checkers were limited to testing small programs written in modeling languages (e.g., Promela). These techniques require that the state of the system has a unique representation that can be kept efficiently in memory. However, applying the same techniques to concurrent programs written in C/C++ is impossible, because the state of each process is too large (e.g., it contains all the memory of the program) and cannot be easily represented as a unique string. VeriSoft solves this problem by keeping no states in memory, albeit, at the risk of more redundant exploration. The stateless search technique makes it feasible to check large programs (e.g., a 2.5 KLOC protocol implementation in C/C++).

The main limitation of stateless search is that it is prone to redundant state exploration (e.g., for a simple example, each state is explored more than 500 times on average). The main problem of stateless search is that it does not impose a strict bound on the amount of redundant work. Indeed, before starting a verification job, there is no guarantee about the amount of time to reach a level of confidence equal to exhaustive search.

VeriSoft handles the exploration of redundant states using partial order reduction. However, this technique cannot handle dynamic dependencies (dynamic dependencies are addressed in a later paper, by the same author, on dynamic partial order reduction) and will not speed up stateless search for any program. For instance, static partial order reduction cannot infer when two different threads or processes can access the same memory (such as an access to an element in a hash table). Thus, static partial order reduction techniques treat the entire hash table as a single variable, and cannot effectively prune the search space.

All the limitations mentioned above suggest that even though model checking has become more practical (e.g., can test real, unmodified code) with the advent of stateless search, it is still not scalable enough to check any of todayʼs complex programs, that have very large state spaces.