Award Abstract # 2303489
POSE: Phase II: An Open-Source Ecosystem for the cvc5 SMT Solver

NSF Org: TI
Translational Impacts
Recipient: THE LELAND STANFORD JUNIOR UNIVERSITY
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 2023 = $1,500,000.00
FY 2024 = $20,000.00
History of Investigator:
  • Clark Barrett (Principal Investigator)
    barrett@cs.stanford.edu
  • Cesare Tinelli (Co-Principal Investigator)
Recipient Sponsored Research Office: Stanford University
450 JANE STANFORD WAY
STANFORD
CA  US  94305-2004
(650)723-2300
Sponsor Congressional District: 16
Primary Place of Performance: Stanford University
450 Jane Stanford Way
Stanford
CA  US  94305-2004
Primary Place of Performance
Congressional District:
16
Unique Entity Identifier (UEI): HJD6G4D6TJY5
Parent UEI:
NSF Program(s): POSE
Primary Program Source: 01002324DB NSF RESEARCH & RELATED ACTIVIT
01002425DB NSF RESEARCH & RELATED ACTIVIT
Program Reference Code(s):
Program Element Code(s): 211Y00
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.

Print this page

Back to Top of page