* ICSE 2018 *
Sun 27 May - Sun 3 June 2018 Gothenburg, Sweden
Thu 31 May 2018 15:00 - 15:30 at E1/B room - Verification Chair(s): Marie-Christine Jakobs

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-based toolchain for incremental checking. Our results show that proof checking with iCoq is up to 10 times faster than the former and up to 3 times faster than the latter.

Slides (rps.pdf)248KiB

Conference Day
Thu 31 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:30
VerificationDEMO - Demonstrations at E1/B room
Chair(s): Marie-Christine JakobsLMU, Munich, Germany
14:00
30m
Talk
COMB: Computing Relevant Program Behaviors
DEMO - Demonstrations
Link to publication
14:30
30m
Demonstration
The Gamma Statechart Composition Framework: Design, Verification and Code Generation for Component-Based Reactive Systems
DEMO - Demonstrations
Vince MolnárBudapest University of Technology and Economics, Bence GraicsBudapest University of Technology and Economics, András VörösBudapest University of Technology and Economics, Istvan MajzikBudapest University of Technology and Economics, Daniel VarroMcGill University / Budapest University of Technology and Economics
DOI Pre-print Media Attached
15:00
30m
Talk
A Regression Proof Selection Tool For Coq
DEMO - Demonstrations
Ahmet CelikUniversity of Texas at Austin, USA, Karl PalmskogThe University of Texas at Austin, Milos GligoricUniversity of Texas at Austin
Pre-print Media Attached File Attached