In: Formal Methods and Software Engineering: 5th International Conference on Formal Engineering Methods, ICFEM 2003, Singapore, November 5-7, 2003, pages 319-337. Volume 2885 of Lecture Notes in Computer Science --- Springer-Verlag, November 2003.
Abstract: The sweep-line method deletes states on-the-fly during state space exploration to reduce peak memory usage. This deletion of states prohibits the immediate generation of, e.g., an error-trace when the violation of a safety property is detected. We address this problem by combining the sweep-line method with storing a spanning tree of the explored state space in external storage on a magnetic disk. We show how this allows us to easily obtain paths in the state space, such as error-traces. A key property of the proposed technique is that it avoids searching in external storage during the state space exploration and gives the same reduction in peak memory usage as the stand-alone sweep-line method. We evaluate the proposed technique on a number of example systems, and compare its performance to a related technique. These practical experiments demonstrate how the suggested technique complements existing techniques based on using external storage.