| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | May 31, 2019 |
| Latest Amendment Date: | April 18, 2024 |
| Award Number: | 1901033 |
| 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: | July 1, 2019 |
| End Date: | December 31, 2024 (Estimated) |
| Total Intended Award Amount: | $1,017,511.00 |
| Total Awarded Amount to Date: | $1,085,511.00 |
| Funds Obligated to Date: |
FY 2021 = $271,531.00 FY 2022 = $282,577.00 FY 2023 = $16,000.00 FY 2024 = $20,000.00 |
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
5000 FORBES AVE PITTSBURGH PA US 15213-3815 (412)268-8746 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
5000 Forbes Ave, WQED Building Pittsburgh PA US 15213-3890 |
| 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 01002223DB NSF RESEARCH & RELATED ACTIVIT 01002122DB 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
Software is becoming ever more essential to society, yet the apps we use continue to be plagued by errors (bugs) that range from inconveniences to severe security threats. Verification is a promising new technology for eliminating bugs from software. But verification is also very expensive--it may cost 10 times the amount of regular software development, making verification way too expensive to fully apply to all software. The project's novelties are based on making verification gradual, so that it can be applied to just part of a software system, not all of it. The project's impacts are based on allowing engineers to focus verification efforts on the most important parts of applications, and on eliminating the bugs that cause the biggest problems. This could eliminate the most severe bugs from software apps with a relatively small increase in cost. The project will also enhance the teaching of verification by providing students with a smoother path to learning the topic, and will take specific steps towards broadening the participation of underrepresented groups in computing.
The project's technical approach builds on recent work on abstracting gradual typing: a principled approach that that applies ideas from abstract interpretation to systematically adapt a static type system into one that allows static and dynamic types to be mixed. We proposed to adapt this approach to make verification gradual. In the gradual verification setting, developers can choose to specify possibly partial pre- and post-condition specifications for the critical functions in a program, while leaving other functions and properties unspecified. The gradual verifier will use abstract interpretation to statically identify inconsistencies between specifications and code, but without triggering false warnings due to specifications that are missing or incomplete. It will also insert the minimum run-time checks that are necessary in order to enforce any properties that the static verifier cannot assure. The approach is being validated through a combination of formative qualitative studies, formalization and proof, prototype implementation and performance evaluation, and summative user studies and case studies.
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.
PROJECT OUTCOMES REPORT
Disclaimer
This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.
Software is becoming more and more important to society--so when it fails due to bugs or security vulnerabilities, the cost is high. Verification is a way to mathematically check that software is free of these costly bugs and vulnerabilities. But verification is expensive, and so it is impractical to apply it everywhere.
In terms of intellectual merit, this project developed Gradual Verification, a new kind of verification that can be applied to programs one piece at a time. This makes verification more practical: software developers can focus on the most important parts of their program first, and get immediate benefit from verifying them. Later, they can verify other parts of their program, or verify the absence of more kinds of bugs. We developed a mathematical model of gradual verification that precisely describes what it is so that engineers in industry can build gradual verification tools—and we used mathematical proof techniques to show that our model makes sense.
We also built a prototype gradual verification tool for C0, a subset of the C programming language that is used in education at Carnegie Mellon University. Next, we used C0 to verify a number of interesting data structures and programs and we measured the performance of verification. Gradual verification does some work when a program is compiled and some work when it is run. Our measurements showed that our approach is effective at using the work done at “compile time” to reduce the work that has to be done at “run time,” producing time savings for engineers.
In terms of broader impacts, the project laid the foundations for new techniques that can make verification more practical. This in turn can reduce the number of bugs in the software that everyone uses, making the public’s experience with software better. The project also contributed to the education of 8 graduate students and 10 undergraduate students. The grad student who led the project finished her Ph.D. and is now a professor at Purdue University, where she is building on the research of the project and teaching her own students to do programming languages research.
Last Modified: 04/29/2025
Modified by: Joshua S Sunshine
Please report errors in award information by writing to: awardsearch@nsf.gov.
