Integrated Concurrency Analysis in a Software Development Environment

对分析、验证和测试的有效支持需要各种技术的协调应用。由于分析并发软件的困难特别严重，因此引入多种技术来解决这个问题就显得特别重要。这个项目将开发并演示一种集成分析技术的通用方法，用于并发软件中同步故障的检测。一组用于分析并发程序的工具组件将嵌入到软件开发环境中。可达性分析技术将用于检测用其他分析和测试技术特别难以检测的故障类（例如竞态条件）。一种新的分治分析技术将被实现。灵活控制工作量/准确性的权衡，以及通过其他分析和测试技术过滤潜在错误报告的选择，将用于控制可达性分析作为一种独立技术的缺点。并发分析工具集将作为研究新技术组合的实验测试平台，包括可达性分析与符号执行的集成。

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.