Explicit-enumeration based Verification made Memory-efficient

We investigate new techniques for reducing the memory requirements of an on-the-fly model checking tool that employs explicit enumeration. Two techniques are studied in depth: exploiting symmetries in the model, and exploiting sequential regions in the model. These techniques can result in a significant reduction in memory requirements, and often find progress violations at much lower stack depths. Both techniques have been implemented as part of the SPIN verifier, a widely used on-the-fly model-checking tool. I. Introduction With the growing complexity of hardware and software systems, there is growing awareness that they must be formally verified. Model-checking [3] is a popular approach for verification, especially for reactive systems. Modelchecking can be done in many ways, two popular methods being implicit enumeration and explicit enumeration. Explicit enumeration proceeds by building the state graph of the model and checking the desired properties on the state graph. Explicit e..