%0 Conference Proceedings
%T Exploiting Transition Locality in Automatic Verification
%A Tronci, Enrico
%A Della Penna, Giuseppe
%A Intrigila, Benedetto
%A Venturini Zilli, Marisa
%Y Margaria, T.
%Y Melham, T.F.
%S 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME)
%S Lecture Notes in Computer Science
%D 2001
%V 2144
%I Springer
%C Livingston, Scotland, UK
%@ 3-540-42541-1
%F Tronci_etal2001
%O exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=44), last updated on Thu, 22 Nov 2012 14:59:18 +0100
%X In this paper we present an algorithm to contrast state explosion when using Explicit State Space Exploration to verify protocols. We show experimentally that protocols exhibit transition locality. We present a verification algorithm that exploits transition locality as well as an implementation of it within the Mur$\varphi$ verifier. Our algorithm is compatible with all Breadth First (BF) optimization techniques present in the Mur$\varphi$ verifier and it is by no means a substitute for any of them. In fact, since our algorithm trades space with time, it is typically most useful when one runs out of memory and has already used all other state reduction techniques present in the Mur$\varphi$ verifier. Our experimental results show that using our approach we can typically save more than 40% of RAM with an average time penalty of about 50% when using (Mur$\varphi$) bit compression and 100% when using bit compression and hash compaction.
%R 10.1007/3-540-44798-9_22
%U http://mclab.di.uniroma1.it/publications/papers/papers/Tronci2001a.pdf
%U https://doi.org/10.1007/3-540-44798-9_22
%P 259-274