View article

Large-scale software verification projects increasingly rely on proof assistants, such as Coq, to construct formal proofs of program correctness. However, such proofs must be checked after every change to a project to ensure expected program behavior. This process of regression proving can require substantial machine time, which is detrimental to productivity and trust in evolving projects. We present iCoq, the first regression proof selection tool. iCoq tracks fine-grained dependencies between Coq definitions, propositions, and proofs, and only checks those proofs affected by changes between two revisions. iCoq is suitable for workflows involving version control and continuous integration services, e.g., Travis CI. We applied iCoq to track dependencies across many revisions in several large Coq projects and measured the time savings compared to proof checking from scratch and when using Coq's timestamp …