Explicit-Enumeration Based Verification
	       Made Memory-Efficient

	
		Ratan Nalumasu

	    Ganesh Gopalakrishnan

		UUCS-95-005

	  Department of Computer Science

	University of Utah, Salt Lake City,

		UT 84112, USA

	Email : {ratan, ganesh} @ cs.utah.edu


		ABSTRACT

    We investigate techniques for reducing the memory requirements
    of a model checking tool employing explicit enumeration.
	Two techniques are studied in depth: (1)~exploiting symmetries in
	the model,
	and (2)~exploiting sequential regions in the model.
    The first technique resulted in a significant reduction in memory
	requirements at the expense of an increase in run time.
    It is capable of finding progress violations
	at much lower stack depths.
    In addition, it is more general than two
  	previously published methods to exploit symmetries, namely
	scalar sets and network invariants.
    The second technique comes with no time overheads and can effect
	significant memory usage reductions directly related to the
	amount of sequentiality in the model.
    Both techniques have been implemented as part of the SPIN verifier.