
NSF Org: |
TI Translational Impacts |
Recipient: |
|
Initial Amendment Date: | August 24, 2023 |
Latest Amendment Date: | March 26, 2024 |
Award Number: | 2303489 |
Award Instrument: | Standard Grant |
Program Manager: |
Florence Rabanal
frabanal@nsf.gov (703)292-8808 TI Translational Impacts TIP Directorate for Technology, Innovation, and Partnerships |
Start Date: | September 1, 2023 |
End Date: | August 31, 2025 (Estimated) |
Total Intended Award Amount: | $1,500,000.00 |
Total Awarded Amount to Date: | $1,520,000.00 |
Funds Obligated to Date: |
FY 2024 = $20,000.00 |
History of Investigator: |
|
Recipient Sponsored Research Office: |
450 JANE STANFORD WAY STANFORD CA US 94305-2004 (650)723-2300 |
Sponsor Congressional District: |
|
Primary Place of Performance: |
450 Jane Stanford Way Stanford CA US 94305-2004 |
Primary Place of
Performance Congressional District: |
|
Unique Entity Identifier (UEI): |
|
Parent UEI: |
|
NSF Program(s): | POSE |
Primary Program Source: |
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.084 |
ABSTRACT
Modern society critically relies on computer systems, but these systems are frequently unreliable. Many techniques that aim to produce more reliable software rely on producing and proving mathematical formulas that capture properties of the software. These formulas are called verification conditions, and the research field of automated reasoning is dedicated to the effort of proving such formulas automatically. In the last two decades, automated reasoning tools have evolved from theoretical curiosities to industrial workhorses, now proving billions of verification conditions daily, for a variety of mission-critical workflows. One of the most successful paradigms for automated reasoning is called satisfiability modulo theories (SMT), and tools using this paradigm are called SMT solvers. The goal of this project to help transition a specific, highly successful, SMT solver project, cvc5, from an academic project to a full-blown open-source ecosystem (OSE), The project's novelties include: establishing and growing this ecosystem; defining and implementing organizational and governance principles and structures; building a broad community of developers and users; and establishing a plan for the sustainability of the tool and its ecosystem. If successful, the project's impact will be considerable, with outcomes including: a thriving international community of developers and users of cvc5; a sustainable plan for ongoing coordination and governance among members in this community; and adoption of industry best-practices for security and code quality in cvc5. All of these will, in turn, positively impact academic and industrial tools and workflows using cvc5, ultimately serving the larger goal of helping improve the robustness and reliability of software.
In order to grow the SMT ecosystem, the project will raise awareness of SMT solvers and their capabilities, make cvc5 available on more platforms and in more contexts, and develop tutorials and other learning materials to make SMT solvers more accessible to a broader audience. To build and grow the community, the project organizes a series of workshops for developers and for users, and establishes organization and governance procedures to onboard new authors and developers. The project address many aspects of project sustainability, including technical debt, security concerns with proof production and checking, and a broad set of monitoring and evaluation procedures.
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.