Sciweavers

CAV
2008
Springer

Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis

14 years 2 months ago
Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
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 slightly larger sequential program PK s such that the analysis of PK s can be used to prove properties about P. The reduction introduces symbolic constants and assume statements in PK s . Thus, any sequential analysis that can deal with these two additions can be extended to handle concurrent programs as well, under the context bound. We give instances of the reduction ...
Akash Lal, Thomas W. Reps
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where CAV
Authors Akash Lal, Thomas W. Reps
Comments (0)