Building systems in proof assistants is challenging for many reasons.
Such systems must tolerate changes gracefully: definitions may be
optimized for performance, new theorems may be added, and the proof
assistant itself may change how tactics work. Proof assistants are also
highly expressive; engineers must ensure that their specifications do not
accidentally allow for undesirable behavior. Furthermore, large-scale
developments often depend on good tactic performance, requiring
developers to reason about low-level performance costs.
To help address these challenges, the
(PE) project is collecting best
practices and building techniques and tools for developing large systems in
the demanding and foundational context of proof assistants.
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.
Karl Palmskog, Ahmet Celik, and Milos Gligoric. piCoq: Parallel Regression Proving for Large-Scale Verification Projects. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), 2018.
Ahmet Celik, Karl Palmskog, and Milos Gligoric. A Regression Proof Selection Tool For Coq. In Proceedings of the International Conference on Software Engineering (ICSE), Demo Papers, 2018.
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Adapting Proof Automation to Adapt Proofs. In Proceedings of the ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), 2018.
Ahmet Celik, Karl Palmskog, and Milos Gligoric. iCoq: Regression proof selection for large-scale verification projects. In Proceedings of 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), Urbana, IL, USA, 2017, pp. 171-182.
- Regression proof selection (iCoq)
- Proof repair (PUMPKIN-PATCH)
- Proof engineering bibliography (proofengineering-bib)
- Survey of proof engineering theory, techniques, tools, and best practices
Proof Engineering is an international collaboration between researchers at
University of Washington (UW), Yale-NUS College (Yale-NUS),
The University of Texas at Austin (UT), and Cornell University (CU).
Many volunteers have helped out on PE projects; we're very grateful for
their contributions! Folks currently working on PE include:
- Ahmet Celik (UT)
- Ryan Doenges (CU)
- Milos Gligoric (UT)
- Dan Grossman (UW)
- Karl Palmskog (UT)
- Talia Ringer (UW)
- Ilya Sergey (Yale-NUS)
- Zach Tatlock (UW)
- James Wilcox (UW)
- Doug Woos (UW)