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.
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.
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.
PE is an international collaboration between researchers at University of Washington, Yale-NUS College, The University of Texas at Austin, and KTH Royal Institute of Technology. People currently working on PE include:
We're very grateful for the contributions of the following people: