Anzeige
Erschienen in:
2010 | OriginalPaper | Buchkapitel
Dynamic Cutoff Detection in Parameterized Concurrent Programs
verfasst von : Alexander Kaiser, Daniel Kroening, Thomas Wahl
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 in software 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 non-recursive Boolean programs run by arbitrarily many parallel threads.