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

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

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.