Specifying, building, verifying, and maintaining software systems using proof assistants such as
Coq, Isabelle/HOL,
and HOL4
enables high trustworthiness, but is currently challenging in many ways.
Proof scripts may break easily when definitions are changed, new theorems may be hard to add,
and updating the proof assistant itself may break existing definitions and proofs.
Proof assistant logics are also highly expressive; engineers must ensure that their
specifications can be satisfied with reasonable effort while disallowing undesirable behavior.
Large-scale projects often require extensive proof automation, forcing
engineers to measure and optimize the performance of low-level reasoning steps.
To help address challenges like these, the
Proof Engineering
(PE) project is collecting best
practices and developing techniques and tools for building large systems in
the demanding and foundational context of proof assistants.
We maintain errata for our proof engineering survey (QED at Large).
If you find any additional errors, please report them as a GitHub issue, as a pull request modifying the errata source file, or by contacting the survey authors directly.
The complete source code for the verified regular expression matcher Coq project used as a motivating example in Chapter 2 of the survey is available on GitHub.
Talia has written a Q&A for the survey, including reading
guides for readers of different backgrounds.
Kush Jain, Karl Palmskog, Ahmet Celik, Emilio Jesús Gallego Arias, and Milos Gligoric mCoq: Mutation Analysis for Coq Verification Projects
International Conference on Software Engineering, Tool Demonstrations Track
(ICSE Demo 2020), 89-92, Seoul, South Korea, July 2020.
Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner REPLICA: REPL Instrumentation for Coq Analysis
International Conference on Certified Programs and Proofs
(CPP 2020), 99-113, New Orleans, LA, USA, January 2020.
Ahmet Celik, Karl Palmskog, Marinela Parovic, Emilio Jesús Gallego Arias, and Milos Gligoric Mutation Analysis for Coq
International Conference on Automated Software Engineering
(ASE 2019), 539-551, San Diego, CA, USA, November 2019.
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman Ornaments for Proof Reuse in Coq
International Conference on Interactive Theorem Proving
(ITP 2019), 26:1-26:19, Portland, OR, USA, September 2019.
Ahmet Celik, Karl Palmskog, and Milos Gligoric A Regression Proof Selection Tool for Coq
International Conference on Software Engineering, Tool Demonstrations Track
(ICSE Demo 2018), 117-120, Gothenburg, Sweden, May 2018.
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman Adapting Proof Automation to Adapt Proofs
International Conference on Certified Programs and Proofs
(CPP 2018), 115-129, Los Angeles, CA, USA, January 2018.
