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.

Della Penna, G., Melatti, I., Intrigila, B., Tronci, E. (2005). Exploiting hub states in automatic verification. In AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS (pp.54-68). BERLIN : SPRINGER-VERLAG BERLIN [10.1007/11562948_7].

Exploiting hub states in automatic verification

INTRIGILA, BENEDETTO;
2005-01-01

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.
Third International Symposium on Automated Technology for Verification and Analysis, ATVA 2005
Taipei, TAIWAN
OCT 04-07, 2005
National Science Council, Taiwan, ROC;Ministry of Education, Taiwan;Institute of Information Science, Academia Sinica, Taiwan;National Taiwan University, NTU, Taiwan;Cadence Design Systems
Rilevanza internazionale
contributo
2005
Settore INF/01 - INFORMATICA
English
Protocol-like systems; Verification Algorithms; Model Checking
Intervento a convegno
Della Penna, G., Melatti, I., Intrigila, B., Tronci, E. (2005). Exploiting hub states in automatic verification. In AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS (pp.54-68). BERLIN : SPRINGER-VERLAG BERLIN [10.1007/11562948_7].
Della Penna, G; Melatti, I; Intrigila, B; Tronci, E
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2108/38417
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact