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

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

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.