Data Flow Analysis for Verifying Properties of Concurrent Programs

In this paper we present an approach, based on data ow analysis, that can provide cost-e ective analysis of concurrent programs with respect to explicitly stated correctness properties. Using this approach, a developer speci es a property of a concurrent programas a pattern of selected program events and asks the analysis to verify that all or no program executions satisfy the given property. We have developed a family of polynomialtime, conservative data ow analysis algorithms that support reasoning about these questions. To overcome the traditional inaccuracies of static analysis, we have also developed a range of techniques for improving the accuracy of the analysis results. One strength of our approach is the exibility 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 pres...

• Type: Conference
• Year: 1994
• Where: SIGSOFT
• Authors: Matthew B. Dwyer, Lori A. Clarke
• Keywords: Analysis Algorithms, Cost-e Ective Analysis, Data Ow Analysis, SIGSOFT 1994, Software Engineering