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.