Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
verfasst von : Akash Lal, Thomas Reps
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
This paper addresses the analysis of concurrent programs with shared memory. Such an analysis is undecidable in the presence of multiple procedures. One approach used in recent work obtains decidability by providing only a partial guarantee of correctness: the approach bounds the number of context switches allowed in the concurrent program, and aims to prove safety, or find bugs, under the given bound. In this paper, we show how to obtain simple and efficient algorithms for the analysis of concurrent programs with a context bound. We give a general reduction from a
concurrent
program
P
, and a given context bound
K
, to a
sequential
program
$P_s^K$
such that the analysis of
$P_s^K$
can be used to prove properties about
P
. We give instances of the reduction for common program models used in model checking, such as Boolean programs and pushdown systems.