Interprocedural Analysis of Concurrent Programs Under a Context Bound
Akash Lal, Tayssir Touili, Nicholas Kidd, Thomas Reps
Analysis of recursive programs in the presence of concurrency and shared memory is undecidable. A common approach is to remove the recursive nature of the program while dealing with concurrency. A different approach is to bound the number of context switches, which has been shown to be very useful for program analysis. In previous work, Qadeer and Rehof  showed that context-bounded analysis is decidable for recursive programs under a finite-state abstraction of program data. In this paper, we generalize their result to infinite-state abstractions, and also provide a new symbolic algorithm for the finite case.
Download this report (PDF)
Return to tech report index