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

Project: Research project

Project Details

Description

It is now widely recognized that increasing the reliability of

concurrent software is one of the most important scientific and

technological challenges in the emerging era of multi-core and

distributed computing. The last decade has seen substantial advances

in automatic verification technology to improve the reliability of

sequential 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 environment

description 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 team

includes graduate and undergraduate students.

StatusFinished
Effective start/end date16/08/1731/07/20

Funding

  • National Science Foundation

Fingerprint

Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.