Exploiting Transition Locality in the Disk Based Murphi Verifier

The main obstruction to automatic verification of Finite State Systems is the huge amount of memory required to complete the verification task (state explosion). This motivates research on distributed as well as disk based verification algorithms. In this paper we present a disk based Breadth First Explicit State Space Exploration algorithm as well as an implementation of it within the Murphi verifier. Our algorithm exploits transition locality to decrease the time overhead due to disk usage. To measure the time speedup due to locality exploitation we compared our algorithm with the previously proposed disk based verification algorithm for Murphi. Our experimental results show that our algorithm is between 3 and 10 times (5 times on average) faster than such previously proposed disk based Murphi. To measure the time overhead due to disk usage we compared our algorithm with RAM based verification using the Murphi verifier with enough memoru to complete the verification task. Our experiemental results show that our algorithm is between 2 and 4 times (3 times on average) slower than (RAM) Murphi with enough RAM memory to complete the verification task at hand.