Explicit-enumeration based verification made memory-efficient

New techniques for reducing the memory requirements of an on-the-fly model checking tool that employs explicit enumeration are investigated: exploiting symmetries in the model, and exploiting sequential regions in themodel.

Abstract

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.