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

FMITF：轨道 II：加强 Coq 证明助手中 CVC4 SMT 求解器的集成

• 批准号: 2019348
• 负责人: Cesare Tinelli
• 金额: $ 10万
• 依托单位: University of Iowa
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-07-01 至 2022-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2019348&HistoricalAwards=false
• 关键词: FMitF; Track; II; Strengthening; integration; FMitF; Track; II; Strengthening; integration

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.

证明助手是交互式软件工具，可帮助计算机科学家和数学家证明数学定理。特别是，它们越来越多地用于帮助开发和形式化计算机科学某些领域的理论基础，例如编程语言，或正式陈述并证明特定软件和硬件的正确性。该项目旨在提高流行的COQ证明助手的自动化水平。该项目的新颖性包括在Coq A有效的自动化鄙视CVC4中充分整合，以证明自动证明某些证明子观念，称为逻辑公式，这可能在COQ的证明会话中出现。提高证明助手的自动化水平将通过使COQ中的证明更容易和乏味来对整个学术界和行业的COQ使用者产生积极影响。通过与工业合作伙伴进行计划的合作，证明与现实问题的整合的优势将对已验证的系统软件构造产生重大影响。减少开发全面验证软件的时间和精力将有助于创建更健壮，可靠和安全的软件系统。研究团队以SMTCOQ COQ COQ插件与外部协作者开发的COQ中的CVC4的先前集成为基础。集成是值得信赖的，因为一旦证明了一个子目标，CVC4就会生成正式的证据，然后在内部进行了SMTCOQ，以证明Coq中的子目标。该项目大大扩展了可以通过添加对用户定义的功能和量词的支持来向CVC4分配到CVC4的类别类别。它还通过提出使子目标可证明的其他假设来扩展CVC4和SMTCOQ，并具有在不坚持亚目标时帮助COQ用户的能力。由于该项目实现的自动化增强功能可以适应其他证明助手，因此该项目总体上也有助于将互动性和自动定理的互动性和自动化定理世界的世界紧密结合在一起。该奖项反映了NSF的法定任务，并通过使用该基金会的知识分子优点和广泛的影响来评估NSF的法定任务，并被视为值得的支持。