In this paper we present a new algorithm to counteract state explosion when using Explicit State Space Exploration to verify protocol-like systems. We sketch the implementation of our algorithm within the Caching Mur psi verifier and give experimental results showing its effectiveness. We show experimentally that, when memory is a scarce resource, our algorithm improves on the time performances of Caching Mur psi verification algorithm, saving between 16% and 68% (45% on average) in computation time.
Exploiting hub states in automatic verification / G., Della Penna; B., Intrigila; Melatti, Igor; Tronci, Enrico. - STAMPA. - 3707:(2005), pp. 54-68. (Intervento presentato al convegno 3rd International Symposium on Automated Technology for Verification and Analysis tenutosi a Taipei, TAIWAN nel OCT 04-07, 2005) [10.1007/11562948_7].
Exploiting hub states in automatic verification
MELATTI, IGOR;TRONCI, Enrico
2005
Abstract
In this paper we present a new algorithm to counteract state explosion when using Explicit State Space Exploration to verify protocol-like systems. We sketch the implementation of our algorithm within the Caching Mur psi verifier and give experimental results showing its effectiveness. We show experimentally that, when memory is a scarce resource, our algorithm improves on the time performances of Caching Mur psi verification algorithm, saving between 16% and 68% (45% on average) in computation time.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
