A tool for proof repair

PUMPKIN PATCH ("Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker") is a tool to extend proof automation in Coq with better support for the evolving nature of software development and verification. This tool is the focus of a research project in the PLSE group of UW CSE. This project is part of a broader effort on research in proof engineering.

To learn more about the current prototype, check out our recent paper in CPP 2018.

Source code

Available on GitHub.



Talia Ringer is the point of contact: tringer@cs.washington.edu.