TY  - CONF
AU  - Tronci, Enrico
AU  - Della Penna, Giuseppe
AU  - Intrigila, Benedetto
AU  - Venturini Zilli, Marisa
PY  - 2001
DA  - 2001//
TI  - A Probabilistic Approach to Automatic Verification of Concurrent Systems
BT  - 8th Asia-Pacific Software Engineering Conference (APSEC)
SP  - 317
EP  - 324
PB  - IEEE Computer Society
CY  - Macau, China
AB  - The main barrier to automatic verification of concurrent systems is the huge amount of memory required to complete the verification task (state explosion). In this paper we present a probabilistic algorithm for automatic verification via model checking. Our algorithm trades space with time. In particular, when memory is full because of state explosion our algorithm does not give up verification. Instead 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 by 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 with enough memory to complete the verification task. This is better than giving up the verification task because of lack of memory.
SN  - 0-7695-1408-1
L1  - http://mclab.di.uniroma1.it/publications/papers/papers/Tronci2001.pdf
UR  - https://doi.org/10.1109/APSEC.2001.991495
DO  - 10.1109/APSEC.2001.991495
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=43), last updated on Thu, 22 Nov 2012 14:59:18 +0100
ID  - Tronci_etal2001
ER  -