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.
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.
Ahmet Celik, Karl Palmskog, Marinela Parovic, Emilio Jesús Gallego Arias and Milos Gligoric. Mutation Analysis for Coq. To appear in Proceedings of the International Conference on Automated Software Engineering (ASE), 2019.
Talia Ringer, Nathaniel Yazdani, John Leo and Dan Grossman. Ornaments for Proof Reuse in Coq. To appear in Proceedings of the International Conference on Interactive Theorem Proving (ITP), 2019.
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 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 the International Conference on Automated Software Engineering (ASE), 2017.
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)