Abstract

Disk based model checking does not receive much attention in the model checking field becasue of its costly time overhead. In this thesis, we present a new disk based algorithm that can get close to or faster verification speed than a RAM based algorithm that has enough memory to complete its verification. This algorithm also outperforms Stern and Dill's original disk based algorithm. The algorithm partitions the state space to several files, and swaps files into and out of memory during verification. Compared with the RAM only algorithm, the new algoritm reduces hash table insertion time by reducing the cost and growth of the hash load. Compared with Stern's disk based algorithm, the new disk based algorithm significantly reduces disk vs memory comparsion but increases disk read/write time. The size of the model the new algorithm can verify is bound to the available disk size instead of the available RAM size.

Degree

College and Department

Physical and Mathematical Sciences; Computer Science

Rights

http://lib.byu.edu/about/copyright/