Proof Engineering

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.

News

May 2020 Extended abstract at Coq Workshop 2020.

Mar 2020 Paper in IJCAR 2020.

Jan 2020 Papers in TACAS 2020 and ICSE-Demo 2020.

Nov 2019 Paper in CPP 2020.

Sep 2019 Paper in FTPL.

Aug 2019 Paper in ASE 2019.

May 2019 Paper in ITP 2019.

Nov 2018 Won a research award from Facebook.

May 2018 Paper in ISSTA 2018.

Feb 2018 Paper in ICSE-Demo 2018.

Nov 2017 Papers in ASE 2017 and CPP 2018.

May 2017 Site goes live.

Errata and resources for proof engineering survey

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.

Publications

Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric
Learning to Format Coq Code Using Language Models
The Coq Workshop
(Coq 2020), Paris, France, July 2020.
Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric
Deep Generation of Coq Lemma Names Using Elaborated Terms
International Joint Conference on Automated Reasoning
(IJCAR 2020), 97-118, Paris, France, July 2020.
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.
Karl Palmskog, Ahmet Celik, and Milos Gligoric
Practical Machine-Checked Formalization of Change Impact Analysis
International Conference on Tools and Algorithms for the Construction and Analysis of Systems
(TACAS 2020), 137-157, 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.
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock
QED at Large: A Survey of Engineering of Formally Verified Software
Foundations and Trends in Programming Languages
(FTPL), Vol. 5: No. 2-3, pp 102-281, September 2019.
Karl Palmskog, Ahmet Celik, and Milos Gligoric
piCoq: Parallel Regression Proving for Large-Scale Verification Projects
International Symposium on Software Testing and Analysis
(ISSTA 2018), 344-355, Amsterdam, The Netherlands, July 2018.
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.
Ahmet Celik, Karl Palmskog, and Milos Gligoric
iCoq: Regression Proof Selection for Large-Scale Verification Projects
International Conference on Automated Software Engineering
(ASE 2017), 171-182, Urbana-Champaign, IL, USA, November 2017.

Current Projects

Proof assistant machine learning datasets (MathComp corpus)
Learning and suggesting proof assistant coding conventions (Roosterize)
Proof assistant change analytics (Coq data)
Mutation proving (mCoq)
Ornamental search (DEVOID)
Survey of proof engineering theory, techniques, tools, and best practices (QED at Large)
Proof checking parallelization (piCoq)
Proof repair (PUMPKIN-PATCH)
Regression proof selection (iCoq and Chip)
Proof engineering bibliography (proofengineering-bib)
Proof document serialization (SerAPI)

Contributors

PE is an international collaboration between researchers at University of Washington, Yale-NUS College, The University of Texas at Austin, KTH Royal Institute of Technology, Inria, and Université de Paris. People currently working on PE include:

We're very grateful for the contributions of the following people: