PT Unknown
AU Tronci, E
   Della Penna, G
   Intrigila, B
   Venturini Zilli, M
TI Exploiting Transition Locality in Automatic Verification
SE 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME)
PY 2001
BP 259
EP 274
VL 2144
DI 10.1007/3-540-44798-9_22
AB 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.
PI Livingston, Scotland, UK
ER