The focus of this research is the static analysis of concurrent software systems. The purpose of this analysis is to determine whether a given program or program specification satisfies certain correctness requirements, such as freedom of deadlock or absence of starvation. The goal of this research project is to define new techniques and automated tools for the analysis of concurrent programs. The new techniques will be aimed at extending and integrating existing analysis methods. To date a number of approaches to the analysis of concurrent programs have been proposed. Some approaches have been implemented and the resulting analysis tools have been tested on some well-known examples of concurrent programs. At present, however, little is known about the types and sizes of programs to which each approach can be usefully applied, and the kinds of questions about the programs that the approach can effectively answer. Some approaches which use linear algebra or temporal logic based techniques to perform portions of the analysis are especially promising. These approaches will be investigated in an effort to characterize their relative strengths and weaknesses. The evaluation of the existing approaches will guide the definition of new analysis techniques. Preliminary investigations in this area have identified various possibilities for extending and integrating existing approaches. The new analysis techniques must be amenable to the implementation of automated analysis tools. Practical experimentations and the evaluation of performance results will play a crucial role when assessing the relative strengths of existing and proposed approaches.
