@InProceedings{DellaPenna_etal2002,
author="Della Penna, Giuseppe
and Intrigila, Benedetto
and Tronci, Enrico
and Venturini Zilli, Marisa",
editor="Aagaard, M.
and O{\textquoteright}Leary, J.W.",
title="Exploiting Transition Locality in the Disk Based Mur{\$}{\backslash}varphi{\$} Verifier",
booktitle="4th International Conference on Formal Methods in Computer-Aided Design (FMCAD)",
series="Lecture Notes in Computer Science",
year="2002",
publisher="Springer",
address="Portland, OR, USA",
volume="2517",
pages="202--219",
abstract="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 Mur{\$}{\backslash}varphi{\$} verifier. Our algorithm exploits transition locality (i.e. the statistical fact that most transitions lead to unvisited states or to recently visited states) to decrease disk read accesses thus reducing the time overhead due to disk usage. A disk based verification algorithm for Mur{\$}{\backslash}varphi{\$} has been already proposed in the literature. To measure the time speed up due to locality exploitation we compared our algorithm with such previously proposed algorithm. Our experimental results show that our disk based verification algorithm is typically more than 10 times faster than such previously proposed disk based verification algorithm. To measure the time overhead due to disk usage we compared our algorithm with RAM based verification using the (standard) Mur{\$}{\backslash}varphi{\$} verifier with enough memory to complete the verification task. Our experimental results show that even when using 1/10 of the RAM needed to complete verification, our disk based algorithm is only between 1.4 and 5.3 times (3 times on average) slower than (RAM) Mur{\$}{\backslash}varphi{\$} with enough RAM memory to complete the verification task at hand. Using our disk based Mur{\$}{\backslash}varphi{\$} we were able to complete verification of a protocol with about {\$}10^9{\$} reachable states. This would require more than 5 gigabytes of RAM using RAM based Mur{\$}{\backslash}varphi{\$}.",
optnote="exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=41), last updated on Sat, 24 Nov 2012 14:28:28 +0100",
issn="3-540-00116-6",
doi="10.1007/3-540-36126-X_13",
opturl="https://doi.org/10.1007/3-540-36126-X_13",
file=":http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2002.pdf:PDF"
}