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

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

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.