Interprocedural Analysis of Concurrent Programs Under a Context Bound
Akash Lal, Tayssir Touili, Nicholas Kidd, and Thomas Reps
Analysis of recursive programs in the presence of concurrency and
shared memory is undecidable. 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 show that context-bounded analysis is decidable for certain
families of infinite-state abstractions, and also provide a new
symbolic algorithm for the finite-state case.
(Click here to access the paper:
PDF.)