Together with Moritz Hammer, I wrote a paper on how to explore very large state spaces: To Store or Not to Store Reloaded: Reclaiming Memory on Demand (accepted for publication to FMICS 2006).

Abstract

Behrmann et al. posed the question whether "To Store or Not To Store" states during reachability analysis, in order to counter the effects of the well-known state space explosion problem in explicit-state model checking. Their answer was to store not all but only some strategical states. They pay in run-time if the answer too often is "Not To Store". We propose a different strategy to adaptively trade time for space: "To Store" as many states as memory limits permit. If memory runs full, we gradually swap states out to secondary storage. We are careful to minimize revisits, and I/O overhead, and also stay sound, i.e. on termination it is guaranteed that the full state space has been explored. It is also available for counterexample reconstruction. In our experiments we tackled state spaces of industrial-sized models with more than 10⁹ explicit states with still modest storage requirements.

We actually have a practical application for this: automatically finding subtle bugs in Embedded Systems software.