Creative Commons Attribution 4.0 license (CC BY 4.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.18
URN: urn:nbn:de:0030-drops-167273
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16727/
Gross, Jason ; Zimmermann, Théo ; Poddar-Agrawal, Miraya ; Chlipala, Adam
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
| pdf-format: |
|
Abstract
As the adoption of proof assistants increases, there is a need for efficiency in identifying, documenting, and fixing compatibility issues that arise from proof-assistant evolution. We present the Coq Bug Minimizer, a tool for reproducing buggy behavior with minimal and standalone files, integrated with coqbot to trigger automatically on failures from Coq’s reverse dependency compatibility testing. Our tool eliminates the overhead of having to download, set up, compile, and then explore and understand large developments, enabling Coq developers to easily obtain modular test-case files for fast experimentation. In this paper, we describe insights about how test-case reduction is different in Coq than in traditional compilers. We expect that our insights will generalize to other proof assistants. We evaluate the Coq Bug Minimizer on over 150 compatibility testing failures. Our tool succeeds in reducing failures to smaller test cases roughly 75% of the time. The minimizer produces a fully standalone test case 89% of the time, and it is on average about one-third the size of the original test. The average reduced test case compiles in 1.25 seconds, with 75% taking under half a second.
BibTeX - Entry
@InProceedings{gross_et_al:LIPIcs.ITP.2022.18,
author = {Gross, Jason and Zimmermann, Th\'{e}o and Poddar-Agrawal, Miraya and Chlipala, Adam},
title = {{Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {18:1--18:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16727},
URN = {urn:nbn:de:0030-drops-167273},
doi = {10.4230/LIPIcs.ITP.2022.18},
annote = {Keywords: debugging, automatic test-case reduction, Coq, bug minimizer}
}
| Keywords: | debugging, automatic test-case reduction, Coq, bug minimizer | |
| Seminar: | 13th International Conference on Interactive Theorem Proving (ITP 2022) | |
| Issue date: | 2022 | |
| Date of publication: | 03.08.2022 | |
| Supplementary Material: |
Dataset (Data and Data Analysis Script): https://doi.org/10.6084/m9.figshare.19141952.v1 Software (Source Code): https://github.com/JasonGross/coq-tools archived at: https://archive.softwareheritage.org/swh:1:dir:eb2345b367437d8b36b80b18a15059673681b22b |
