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

点击翻译按钮获取中文摘要

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.