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.
Status | Finished |
---|---|
Effective start/end date | 16/08/17 → 31/07/20 |
Funding
- National Science Foundation