FMitF: Track II: Strengthening the integration of the CVC4 SMT solver in the Coq proof assistant

证明助手是帮助计算机科学家和数学家证明数学定理的交互式软件工具。特别是，它们越来越多地被用来帮助开发和形式化某些计算机科学领域的理论基础，例如编程语言，或者正式地陈述和证明特定软件和硬件的正确性。本项目旨在提高目前流行的CoQ证明助手的自动化水平。该项目的创新之处在于在Coq中完全集成了一个强大的自动证明器CVC4，以自动证明某些表示为逻辑公式的证明子目标，这些子目标可能在Coq中的证明过程中出现。提高校样助手的自动化水平将使CoQ中的校样开发变得更容易、更少繁琐，从而对整个学术界和行业的CoQ用户产生积极影响。通过与行业合作伙伴的有计划的协作来展示这种与真实世界问题集成的优势，将对系统软件的验证构建产生重大影响。减少开发完全验证软件的时间和精力将有助于创建更健壮、可靠和安全的软件系统。研究团队建立在之前通过与外部合作者开发的SMTCoq Coq插件实现的Coq中CVC4集成的基础上。这种集成是值得信赖的，因为一旦它验证子目标，CVC4就会生成一个正式的证明，然后SMTCoq在内部回放以证明Coq内的子目标。该项目通过添加对用户定义函数和量词的支持，极大地扩展了可以分派到CVC4的子目标类。它还扩展了CVC4和SMTCoq，使其能够在子目标不成立时帮助Coq用户，方法是提出使该子目标可证明的附加假设。由于这个项目实现的自动化增强可以适用于其他证明助手，这个项目总体上也有助于拉近交互和自动化定理证明的世界。这个奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Proof assistants are interactive software tools that help computer scientists and mathematicians prove mathematical theorems. In particular, they are increasingly used to help develop and formalize the theoretical foundations of certain areas of computer science, such as programming languages, or formally state and prove the correctness of specific software and hardware. This project aims to improve the level of automation in the popular Coq proof assistant. The project's novelty consists in fully integrating in Coq a powerful automated prover, CVC4, to prove automatically certain proof subgoals, expressed as logical formulas, that may arise during a proof session in Coq. Increasing the level of automation in proof assistants will positively impact Coq users throughout academia and industry by making it easier and less tedious to develop proofs in Coq. Demonstrating the advantages of this integration with real-world problems through a planned collaboration with an industrial partner will have a significant impact on verified construction of systems software. The reduction of time and effort to develop fully verified software will facilitate the creation of more robust, reliable and secure software systems.The research team builds on a previous integration of CVC4 in Coq achieved through the SMTCoq Coq plugin developed with external collaborators. The integration is trustworthy because, once it proves a subgoal, CVC4 generates a formal proof that SMTCoq then replays internally to prove the subgoal within Coq. This project significantly extends the class of subgoals that can be dispatched to CVC4 by adding support for user-defined functions and quantifiers. It also extends CVC4 and SMTCoq with the ability to help the Coq user when a subgoal does not hold, by suggesting additional assumptions that would make the subgoal provable. Since the sort of automation enhancements achieved with this project could be adapted to other proof assistants, this project also contributes in general to bringing closer together the worlds of interactive and automated theorem proving.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.