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.
(Click here to access the paper:
PDF]