Show simple item record

dc.contributor.authorLal, Akashen_US
dc.contributor.authorReps, Thomasen_US
dc.description.abstractThis 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 P_s^K such that the analysis of P_s^K can be used to prove properties about P. The reduction introduces symbolic constants and \assume statements in P_s^K. 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 for common program models used in model checking, such as Boolean programs, pushdown systems (PDSs), and symbolic PDSs.en_US
dc.publisherUniversity of Wisconsin-Madison Department of Computer Sciencesen_US
dc.titleReducing Concurrent Analysis Under a Context Bound to Sequential Analysisen_US
dc.typeTechnical Reporten_US

Files in this item


This item appears in the following Collection(s)

  • CS Technical Reports
    Technical Reports Archive for the Department of Computer Sciences at the University of Wisconsin-Madison

Show simple item record