| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | June 14, 2019 |
| Latest Amendment Date: | June 14, 2019 |
| Award Number: | 1909862 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Anindya Banerjee
abanerje@nsf.gov (703)292-7885 CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | October 1, 2019 |
| End Date: | April 30, 2021 (Estimated) |
| Total Intended Award Amount: | $250,000.00 |
| Total Awarded Amount to Date: | $250,000.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
107 S INDIANA AVE BLOOMINGTON IN US 47405-7000 (317)278-3473 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
700 N. Luddy Hall, Rm 3024 Bloomington IN US 47401-3654 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | Software & Hardware Foundation |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
Formal verification promises to deliver software that works precisely according to a given mathematical specification. The last decade has seen several impressive formally verified software artifacts that are provably free of large classes of defects. However, these artifacts required Herculean feats of engineering, using specialized proof assistants that are separated, by a wide chasm, from the legacy languages and libraries that are used to engineer efficient parallel software. This project's novelties are in new techniques to enable the development of efficient parallel computing systems with formal assurances about correctness and reliability. This project's impacts will be to make formal verification a part of mainstream software development.
This project will build on two approaches discovered by the investigators. The first is refinement reflection, which turns existing programming languages into theorem provers, where the proofs are merely programs in that same language. Second, the investigators have introduced lattice variables, scheduling algorithms and a new linear type system to simplify the construction of efficient parallel software with well-defined behavior. This project will combine the above ideas into a framework wherein engineers can develop and verify parallel software, simply by writing programs in their host language, thereby economically integrating formal proofs within existing software development cycles.
This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.
Please report errors in award information by writing to: awardsearch@nsf.gov.
