| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | April 12, 2021 |
| Latest Amendment Date: | April 30, 2024 |
| Award Number: | 2107206 |
| Award Instrument: | Continuing 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: | May 1, 2021 |
| End Date: | April 30, 2025 (Estimated) |
| Total Intended Award Amount: | $539,956.00 |
| Total Awarded Amount to Date: | $539,956.00 |
| Funds Obligated to Date: |
FY 2022 = $105,412.00 FY 2024 = $108,638.00 |
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
3112 LEE BUILDING COLLEGE PARK MD US 20742-5100 (301)405-6269 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
MD US 20742-3370 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | Software & Hardware Foundation |
| Primary Program Source: |
01002223DB NSF RESEARCH & RELATED ACTIVIT 01002324DB NSF RESEARCH & RELATED ACTIVIT 01002425DB NSF RESEARCH & RELATED ACTIVIT |
| 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 of software in a proof assistant (such as Coq) can establish the correctness of software, preventing software bugs that could otherwise lead to significant financial losses or even loss of life. Unfortunately, proof assistants are not currently well adapted to large-scale software development and are expensive to use in terms of both development time and expertise. The goal of this project is to increase productivity of proof engineers (i.e., users of proof assistants) via techniques that simplify development and maintenance of large verification projects, as well as to increase trustworthiness in the toolchain commonly used by proof engineers. The project's novelties include learning-based and analytical approaches for proof construction, extraction, and maintenance, as well as testing techniques for establishing the trustworthiness of proof assistants. The project's impacts are increased productivity and increased software quality.
This project develops techniques that help proof engineers (1) construct proofs by learning and enforcing conventions, automatically locating relevant lemmas, and synthesizing generalized invariants; (2) augment the extraction of executable code from verified artifacts with runtime monitoring for checking assumption violations and with novel support for generating executable variants of logical specifications; and (3) facilitate the maintenance of large proof repositories by detecting brittle proof scripts, as well as learning common transformations. Furthermore, to increase trust in the proof engineering toolchain, the investigators develop testing techniques that target the core components of proof assistants.
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.
PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH
Note:
When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external
site maintained by the publisher. Some full text articles may not yet be available without a
charge during the embargo (administrative interval).
Some links on this page may take you to non-federal websites. Their policies may differ from
this site.
Please report errors in award information by writing to: awardsearch@nsf.gov.
