Relational interprocedural verification of concurrent programs

摘要

We propose a general analysis method for recur-sive, concurrent programs that track effectively procedure calls and return in a concurrent context, even in the pres-ence of unbounded recursion and infinite-state variables like integers. This method generalizes the relational interproce-dural analysis of sequential programs to the concurrent case, and extends it to backward or coreachability analysis. We implemented it for programs with scalar variables and exper-imented with several classical synchronization protocols in order to illustrate the precision of our technique and also to analyze the approximations it performs.