CAREER: Engineering High-Quality Concurrent Software

一个综合的研究项目将开发用于构建并发软件的技术，以及用于指定并发软件的属性和验证并发软件的技术。并发软件的构建是由工程协调抽象支持的，这些抽象捕获了通信、同步和过程间连通性的公共模式。这项工作的重点是开发抽象，以满足一类现实世界问题的需要，特别是科学计算问题。通过将这些抽象应用于实际问题的解决方案来评估它们的有效性。使用抽象和可选的并发编程技术开发的解决方案的开发成本的度量将形成经验评估的基础，以表征协调抽象的相对优点。利用FLAVERS程序流分析方法研究了并发软件正确性规范的验证。这项工作的重点是在FLAVERS中加入抽象，以提高分析的速度和分析结果的准确性。对FLAVERS有效性的评估是通过将其应用于正确性属性的常见类的验证以及实际并发应用程序（例如使用协调抽象构建的应用程序）来进行的。

An integrated program of research will develop techniques for building concurrent software and techniques for specifying properties of and validating concurrent software. The construction of concurrent software is supported by engineering coordination abstractions that capture common patterns of communication, synchronization and process inter- connectivity. This work focuses on development of abstractions that satisfy the needs of a class of real-world problems, specifically scientific computing problems. The effectiveness of these abstractions is evaluated by applying them to the solution of real-world problems. Measurement of development costs for solutions developed using abstractions and alternative concurrent programming technologies will form the basis of empirical evaluation to characterize the relative merits of coordination abstractions. The validation of specifications of correctness properties of concurrent software is investigated using a program flow analysis called FLAVERS. This work focuses on incorporation of abstractions in FLAVERS to increase both the speed of analysis and the accuracy of analysis results. Evaluation of the effectiveness of FLAVERS is assessed by applying it to the verification of common classes of correctness properties and to real-world concurrent applications, such as those built with coordination abstractions.