Skip directly to content

Minimize RSR Award Detail

Research Spending & Results

Award Detail

Awardee:STEVENS INSTITUTE OF TECHNOLOGY (INC)
Doing Business As Name:Stevens Institute of Technology
PD/PI:
  • Eric Koskinen
  • (201) 669-1206
  • eric.koskinen@stevens.edu
Award Date:12/01/2017
Estimated Total Award Amount: $ 65,597
Funds Obligated to Date: $ 65,597
  • FY 2016=$65,597
Start Date:08/16/2017
End Date:07/31/2019
Transaction Type:Grant
Agency:NSF
Awarding Agency Code:4900
Funding Agency Code:4900
CFDA Number:47.070
Primary Program Source:040100 NSF RESEARCH & RELATED ACTIVIT
Award Title or Description:SHF: Small: Collaborative Research: Concurrent Software Verification with Rely/Guarantee Abstraction
Federal Award ID Number:1813745
DUNS ID:064271570
Parent DUNS ID:064271570
Program:SOFTWARE & HARDWARE FOUNDATION
Program Officer:
  • Nina Amla
  • (703) 292-8910
  • namla@nsf.gov

Awardee Location

Street:CASTLE POINT ON HUDSON
City:HOBOKEN
State:NJ
ZIP:07030-5991
County:Hoboken
Country:US
Awardee Cong. District:08

Primary Place of Performance

Organization Name:Stevens Institute of Technology
Street:
City:
State:NJ
ZIP:07030-5991
County:Hoboken
Country:US
Cong. District:08

Abstract at Time of Award

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.

For specific questions or comments about this information including the NSF Project Outcomes Report, contact us.