The Community for Technology Leaders
2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE) (2017)
Urbana, IL, USA
Oct. 30, 2017 to Nov. 3, 2017
ISBN: 978-1-5386-3976-4
pp: 171-182
Ahmet Celik , University of Texas at Austin, Austin, TX-78712, USA
Karl Palmskog , University of Illinois at Urbana-Champaign, Urbana, IL-61801, USA
Milos Gligoric , University of Texas at Austin, Austin, TX-78712, USA
ABSTRACT
Proof assistants such as Coq are used to construct and check formal proofs in many large-scale verification projects. As proofs grow in number and size, the need for tool support to quickly find failing proofs after revising a project increases. We present a technique for large-scale regression proof selection, suitable for use in continuous integration services, e.g., Travis CI. We instantiate the technique in a tool dubbed iCoq. iCoq tracks fine-grained dependencies between Coq definitions, propositions, and proofs, and only checks those proofs affected by changes between two revisions. iCoq additionally saves time by ignoring changes with no impact on semantics. 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-based toolchain for incremental checking. Our results show that proof checking with iC oq is up to 10 times faster than the former and up to 3 times faster than the latter.
INDEX TERMS
Tools, Java, Time measurement, Software, Standards, Semantics
CITATION

A. Celik, K. Palmskog and M. Gligoric, "ICoq: Regression proof selection for large-scale verification projects," 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), Urbana, IL, USA, 2017, pp. 171-182.
doi:10.1109/ASE.2017.8115630
182 ms
(Ver 3.3 (11022016))