QED at Large: A Survey of Engineering of Formally Verified Software
arXiv:2003.06458 · doi:10.1561/2500000045
Abstract
Development of formal proofs of correctness of programs can increase actual and perceived reliability and facilitate better understanding of program specifications and their underlying assumptions. Tools supporting such development have been available for over 40 years, but have only recently seen wide practical use. Projects based on construction of machine-checked formal proofs are now reaching an unprecedented scale, comparable to large software projects, which leads to new challenges in proof development and maintenance. Despite its increasing importance, the field of proof engineering is seldom considered in its own right; related theories, techniques, and tools span many fields and venues. This survey of the literature presents a holistic understanding of proof engineering for program correctness, covering impact in practice, foundations, proof automation, proof organization, and practical proof development.
arXiv comment183 pages, for errata see https://proofengineering.org/qed_errata.html
References in corpus (23)
- Automatic Software Repair: a Bibliography
- A formal proof of the four color theorem
- Learning-Assisted Automated Reasoning with Flyspeck
- General Recursion via Coinductive Types
- DeepMath - Deep Sequence Models for Premise Selection
- GamePad: A Learning Environment for Theorem Proving
- Verifying Strong Eventual Consistency in Distributed Systems
- Machine Learning in Proof General: Interfacing Interfaces
- QED at Large: A Survey of Engineering of Formally Verified Software
- Isabelle: The Next 700 Theorem Provers
- LISA -- A Modern Proof System
- Deciding Kleene Algebras in Coq
- Developing Bug-Free Machine Learning Systems With Formal Mathematics
- Premise Selection for Theorem Proving by Deep Graph Embedding
- Tactics for Reasoning modulo AC in Coq
- Defining Functions on Equivalence Classes
- Asynchronous processing of Coq documents: from the kernel up to the user interface
- Gradual Certified Programming in Coq
- Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant
- PIDE as front-end technology for Coq
- Algebraic Foundations of Proof Refinement
- A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom
- Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
Cited by in corpus (10)
- QED at Large: A Survey of Engineering of Formally Verified Software
- Towards AI-Assisted Synthesis of Verified Dafny Methods
- Passport: Improving Automated Formal Verification Using Identifiers
- Proof Repair across Type Equivalences
- Maintaining a Library of Formal Mathematics
- Lessons from Formally Verified Deployed Software Systems (Extended version)
- QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
- CoqPilot, a plugin for LLM-based generation of proofs
- Towards Automatic Transformations of Coq Proof Scripts
- A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants