ECOOP 2018
Sun 15 - Sat 21 July 2018 Amsterdam, Netherlands
co-located with ECOOP and ISSTA 2018
Wed 18 Jul 2018 15:00 - 15:20 at Zurich II - Optimization and Performance Chair(s): Tevfik Bultan

Large-scale verification projects using proof assistants typically contain many proofs that must be checked at each new project revision. While proof checking can sometimes be parallelized at the coarse-grained file level to save time, recent changes in some proof assistant in the LCF family, such as Coq, enable fine-grained parallelism at the level of proofs. However, these parallel techniques are not currently integrated with regression proof selection, a technique that checks only the subset of proofs affected by a change. We present techniques that blend the power of parallel proof checking and selection to speed up regression proving in verification projects, suitable for use both on users’ own machines and in workflows involving continuous integration services. We implemented the techniques in a tool, piCoq, which supports Coq projects. piCoq can track dependencies between files, definitions, and lemmas and perform parallel checking of only those files or proofs affected by changes between two project revisions. We applied piCoq to perform regression proving over many revisions of several large open source projects and measured the proof checking time. While gains from using proof-level parallelism and file selection can be considerable, our results indicate that proof-level parallelism and proof selection is consistently much faster than both sequential checking from scratch and sequential checking with proof selection. In particular, 4-way parallelization is up to 28.6 times faster than the former, and up to 2.8 times faster than the latter.

Wed 18 Jul
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:30: ISSTA Technical Papers - Optimization and Performance at Zurich II
Chair(s): Tevfik BultanUniversity of California, Santa Barbara
issta-2018-Technical-Papers14:00 - 14:20
Yingjun LyuUniversity of Southern California, Ding LiNEC Labs, William G.J. HalfondUniversity of Southern California
issta-2018-Technical-Papers14:20 - 14:40
Yannic NollerHumboldt-Universität zu Berlin, Rody KerstenSynopsys, Inc., Corina S PasareanuNASA Ames Research Center
issta-2018-Technical-Papers14:40 - 15:00
Hui GuoUniversity of California, Davis, Cindy Rubio-GonzálezUniversity of California, Davis
issta-2018-Technical-Papers15:00 - 15:20
Karl PalmskogUniversity of Texas at Austin, Ahmet CelikUniversity of Texas at Austin, USA, Milos GligoricUniversity of Texas at Austin
issta-2018-Technical-Papers15:20 - 15:30