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
New Orleans, LA, December 1994, pp. 62-75.
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
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
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
Last modified: Thu Jan 26 13:36:13 1995