"To Store or not to Store" Reloaded: Reclaiming Memory on Demand

Moritz Hammer and Michael Weber

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 free memory becomes scarce, 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-scale models with more than 10⁹ explicit states with still modest storage requirements.

Won the EASST Best Paper Award for the FMICS 2006 workshop.

[PDF], [PS]

A shortened version appeared in the EASST newsletter 2006 - 14.

Reference

@inproceedings {
    hammerweber06tostore,
    author={Moritz Hammer and Michael Weber},
    title={``{To} Store Or Not To Store Reloaded'': Reclaiming Memory On Demand},
    editor={Lubos Brim and Boudewijn Haverkort and Martin Leucker and Jaco van de Pol},
    booktitle={Formal Methods: Application and Technology (FMICS'2006)},
    series={Lecture Notes in Computer Science},
    volume={4346},
    pages={51--66},
    publisher={Springer-Verlag},
    year={2006}
}

Moritz Hammer

Last modified: Thu Apr 5 14:12:50 CEST 2007