论文标题
证明助手的自动测试案例减少：COQ中的案例研究
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
论文作者
论文摘要
随着证明助手的采用增加，需要效率来识别，记录和解决助手演变引起的兼容性问题。我们提出了COQ Bug Minimizer，这是一种用最小和独立文件重现错误行为的工具，并与Coqbot集成了以自动触发COQ RECERSE CI FAILURES上的触发。我们的工具消除了必须下载，设置，编译，然后探索和理解大型开发的开销：使COQ开发人员能够轻松获取模块化测试案例文件进行快速实验。在本文中，我们描述了有关COQ中测试案例减少与传统编译器中如何不同的见解。我们希望我们的见解将推广到其他证明助手。我们评估了150多个CI失败的COQ最小化器。在大约75％的时间内，我们的工具成功地减少了较小的测试用例。最小化器的时间为89％，平均是原始测试的大小约为三分之一。平均减少的测试用例在1.25秒内编译，其中75％的时间不到半秒。
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 Coq reverse CI failures. 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 CI failures. Our tool succeeds in reducing failures to smaller test cases in 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.
