Sciweavers

CAV
2010
Springer

Dynamic Cutoff Detection in Parameterized Concurrent Programs

13 years 7 months ago
Dynamic Cutoff Detection in Parameterized Concurrent Programs
We consider the class of finite-state programs executed by an unbounded number of replicated threads communicating via shared variables. The thread-state reachability problem for this class is essential are verification using predicate abstraction. While this problem is decidable via Petri net coverability analysis, techniques solely based on coverability suffer from the problem's exponential-space complexity. In this paper, we present an alternative method based on a thread-state cutoff : a number n of threads that suffice to generate all reachable thread states. We give a condition, verifiable dynamically during reachability analysis for increasing n, that is sufficient to conclude that n is a cutoff. We then make the method complete, via a coverability query that is of low cost in practice. We demonstrate the efficiency of the approach on Petri net encodings of communication protocols, as well as on nonrecursive Boolean programs run by arbitrarily many parallel threads.
Alexander Kaiser, Daniel Kroening, Thomas Wahl
Added 02 Sep 2010
Updated 02 Sep 2010
Type Conference
Year 2010
Where CAV
Authors Alexander Kaiser, Daniel Kroening, Thomas Wahl
Comments (0)