The main obstruction to automatic verification of Concurrent Systems is is the huge amount of memory required to complete the verification task (state explosion). In fact when the memory is over we are forced to abandon our verification effort, even when we are somehow close to finish it. We believe that waiting longer for a reasonable answer is better than being left with an out of memory message and no answer at all. Thus in this paper we present a probabilistic algorithm for Explicit State Space Exploration. Our algorithm trades space with time. In particular when our memory is over our algorithm does not give up verification. It just proceeds at a lower speed and its results will only hold with some arbitrarily small error probability. Our preliminary experimental results show that using our probabilistic algorithm we can typically save more than 30% of RAM with an average time penalty of about 100% w.r.t. a deterministic state space exploration.

A Probabilistic Approach to Automatic Formal Verification

DELLA PENNA, GIUSEPPE;
2001-01-01

Abstract

The main obstruction to automatic verification of Concurrent Systems is is the huge amount of memory required to complete the verification task (state explosion). In fact when the memory is over we are forced to abandon our verification effort, even when we are somehow close to finish it. We believe that waiting longer for a reasonable answer is better than being left with an out of memory message and no answer at all. Thus in this paper we present a probabilistic algorithm for Explicit State Space Exploration. Our algorithm trades space with time. In particular when our memory is over our algorithm does not give up verification. It just proceeds at a lower speed and its results will only hold with some arbitrarily small error probability. Our preliminary experimental results show that using our probabilistic algorithm we can typically save more than 30% of RAM with an average time penalty of about 100% w.r.t. a deterministic state space exploration.
2001
0-7695-1408-1
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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/11697/30520
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 24
  • ???jsp.display-item.citation.isi??? 12
social impact