POSE: Phase II: An Open-Source Ecosystem for the cvc5 SMT Solver

POSE：第二阶段：cvc5 SMT 求解器的开源生态系统

• 批准号: 2303489
• 负责人: Clark Barrett
• 金额: $ 150万
• 依托单位: Stanford University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-09-01 至 2025-08-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2303489&HistoricalAwards=false
• 关键词: POSE; Phase; II; Open; Source

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.

现代社会严重依赖计算机系统，但这些系统常常不可靠。 许多旨在生成更可靠软件的技术都依赖于生成和证明捕获软件属性的数学公式。 这些公式称为验证条件，自动推理的研究领域致力于自动证明这些公式。 在过去的二十年中，自动推理工具已经从理论上的好奇心发展成为工业主力，现在每天为各种关键任务工作流程提供数十亿个验证条件。 自动推理最成功的范式之一称为可满足性模理论 (SMT)，使用该范式的工具称为 SMT 求解器。 该项目的目标是帮助将一个特定的、非常成功的 SMT 求解器项目 cvc5 从学术项目转变为成熟的开源生态系统 (OSE)。该项目的新颖之处包括：建立和发展这个生态系统；定义和实施组织和治理原则和结构；建立广泛的开发者和用户社区；并制定该工具及其生态系统的可持续性计划。 如果成功，该项目的影响将是巨大的，其成果包括： 一个由 cvc5 开发者和用户组成的蓬勃发展的国际社区；该社区成员之间持续协调和治理的可持续计划；并采用 cvc5 中安全性和代码质量的行业最佳实践。 所有这些反过来都会对使用 cvc5 的学术和工业工具和工作流程产生积极影响，最终服务于帮助提高软件的稳健性和可靠性的更大目标。为了发展 SMT 生态系统，该项目将提高对 SMT 求解器的认识及其功能，使 cvc5 在更多平台和更多环境中可用，并开发教程和其他学习材料，使 SMT 求解器更容易为更广泛的受众所使用。 为了建立和发展社区，该项目为开发人员和用户组织了一系列研讨会，并建立了组织和治理程序来吸引新作者和开发人员。该项目解决了项目可持续性的许多方面，包括技术债务、证明制作和检查的安全问题，以及广泛的监测和评估程序。该奖项反映了 NSF 的法定使命，并通过使用基金会的知识进行评估，被认为值得支持。优点和更广泛的影响审查标准。