Effective support for analysis, verification, and testing requires coordinated application of a variety of techniques. As the difficulties of analyzing concurrent software are especially severe, so it is especially important that multiple techniques be brought to bear on the problem. This project will develop and demonstrate a general approach to integrating analysis techniques applied to the detection of synchronization faults in concurrent software. A set of tool components for analysis of concurrent programs will be embedded in a software development environment. A reachability analysis technique will be used to detect classes of faults (race conditions, for instance) that are particularly difficult to detect with other analysis and testing techniques. A new technique for divide-and- conquer analysis will be implemented. Flexible control of effort/accuracy tradeoffs and the option of filtering reports of potential errors through other analysis and testing techniques will be used to control the shortcomings of reachability analysis as a stand- alone technique. The concurrency analysis tool set will serve as an experimental test-bed for investigating novel combinations of techniques, including integration of reachability analysis with symbolic execution.
