Interprocedural analysis and the verification of concurrent programs

This dissertation addresses program verification by considering two important features of programs: (i) procedures (and procedure calls) and (ii) concurrency.;An analysis that can precisely handle the procedural aspect of programs is called an interprocedural analysis. The dissertation makes several contributions to interprocedural analyses of programs: (1) We define the Extended Weighted Pushdown System (EWPDS) model, which provides a convenient abstraction mechanism for multi-procedure programs. We show that EWPDSs enable several different interprocedural analyses. (2) We use graph-theoretic algorithms to speed up the analysis of EWPDSs. This results in immediate speedup in all of the applications based on EWPDSs. (3) We show how to answer expressive queries on EWPDSs, such as computing the set of all error traces in the model, called an error projection. This enables faster verification.;The dissertation also studies the problem of context-bounded analysis (CBA): the analysis of multi-procedure concurrent programs under a bound on the number of context switches between threads.;CBA is an interesting avenue of research that has attracted a lot of attention recently because empirical evidence suggests that many concurrency-related bugs can be found in a few context switches.;We show that it is possible to automatically extend most interprocedural-analysis techniques for sequential programs to perform CBA. In particular, the dissertation makes two important contributions to CBA: (1) We give sufficient conditions for the decidability of CBA. We also give an algorithm for performing CBA using any abstraction that satisfies these conditions. (2) We show that, given a concurrent program P and a context bound K, one can create a sequential program PK such that the analysis of PK is sufficient for CBA of P under the bound K. We implemented this technique and conducted a study on concurrent Linux drivers to show that most bugs could not only be found in a few context switches, but, compared to previous approaches, they could be found must faster using our approach.