Experiments with Modular FLAVERS Analysis

Analyzing the potential behavior of concurrent software is a difficult and complex problem. In this paper, we describe an analysis approach that takes advantage of the modular structure of complex software systems to reduce the cost of analysis. This work builds off of an existing approach, FLAVERS, that uses program flow analysis to verify explicitly stated correctness properties of concurrent software. We describe three mechanisms through which a modular flow analysis can be formulated by using: sub-system specifications, results of previous analyses, or a sub-system implementation to define analysis boundaries within which an independent flow analysis can be conducted. Using the FLAVERS toolset we report on the application of our modular analysis to selected concurrent programs. We demonstrate that the cost of such a modular analysis is much less than the cost of an analysis of the whole program. We also illustrate how this cost savings can be applied to produce analysis results of ..