Arcadia Papers: ABSTRACT

"Data Flow Analysis for Verifying Properties of Concurrent Programs", by Matthew B. Dwyer and Lori A. Clarke in Proceedings of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering, New Orleans, LA, December 1994, pp. 62-75.

Abstract

In this paper we present an analysis approach based on data flow analysis that has the potential to provide cost-effective analysis of concurrent programs with respect to explicitly stated correctness properties. Using this approach, developers specify properties of concurrent programs as patterns of selected program events and choose whether the analysis should attempt to verify that all or no program executions satisfy the given property. We have developed a family of polynomial-time, conservative data flow analysis algorithms whose results can be used to address such questions.

To overcome the traditional inaccuracies of static analysis, we have also developed a range of techniques for improving the accuracy of the results. Prior to analysis, refinements to the flow graph representation of the program, based on program and property specific information, increase the efficiency of the subsequent analysis and the accuracy of the results. During analysis, enforcement of feasibility constraints, which are based on the program being analyzed and the programming language in which it is written, improves the accuracy of the results. One strength of our approach is the flexibility allowed in choosing and combining these techniques so as to increase accuracy without making analysis time impractical.

We have implemented a prototype toolset that automates the analysis for programs with explicit tasking and rendezvous style communication. We present preliminary experimental results using this toolset.

The Arcadia Project <arcadia-www@ics.uci.edu>
Last modified: Thu Jan 26 13:36:13 1995