Proceedings Eighth Asia-Pacific Software Engineering Conference
Download PDF

Abstract

The main obstruction to automatic verification of concurrent systems is the huge amount of memory required to complete the verification task (state explo- sion). In this paper we present a probabilistic algorithm for automatic verification via model checking. Our algorithm trades space with time. In particular, when our memory is over 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 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 having to give up the verification task because of lack of memory.
Like what you’re reading?
Already a member?Sign In
Member Price
$11
Non-Member Price
$21
Add to CartSign In
Get this article FREE with a new membership!