SHF: Small: Collaborative Research: Concurrent Software Verification with Rely/Guarantee Abstractions

SHF：小型：协作研究：具有依赖/保证抽象的并发软件验证

• 批准号: 1618059
• 负责人: Thomas Wies
• 金额: $ 24.03万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-08-01 至 2020-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1618059&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Concurrent

It is now widely recognized that increasing the reliability ofconcurrent software is one of the most important scientific andtechnological challenges in the emerging era of multi-core anddistributed computing. The last decade has seen substantial advancesin automatic verification technology to improve the reliability ofsequential programs, and software tools that can be applied to large industrial code bases. Unfortunately, the underlying technology of such tools cannot be directly applied to concurrent programs. This project investigates scalable techniques for automatic verification of concurrent software. The approach uses thread-modular decomposition of the overall problem that does not completely decompose to the granularity of an individual thread. Since base components may exhibit concurrent behavior, the investigators develop analysis algorithms for these base components so that they can be automatically proven correct with respect to their environmentdescription and vice-versa. This work yields automatic verification tools that exploit richer notions of modular reasoning about parallelism, thereby offering improved scalability and robustness over previous approaches. The project teamincludes graduate and undergraduate students.

现在人们普遍认识到，在多核和分布式计算的新兴时代，提高并发软件的可靠性是最重要的科技挑战之一。在过去的十年中，自动验证技术有了长足的进步，以提高顺序程序的可靠性，以及可以应用于大型工业代码库的软件工具。不幸的是，这些工具的底层技术不能直接应用于并发程序。该项目研究用于并发软件自动验证的可伸缩技术。该方法使用线程模块分解整个问题，而不是完全分解到单个线程的粒度。由于基本组件可能表现出并发行为，研究人员开发了这些基本组件的分析算法，以便可以自动证明它们在环境描述方面是正确的，反之亦然。这项工作产生了自动验证工具，这些工具利用了关于并行性的更丰富的模块化推理概念，从而提供了比以前的方法更好的可扩展性和健壮性。该项目团队包括研究生和本科生。