一句话：提出变异证明技术并实现 mCoq，通过变异 Coq 定义检验证明是否失败，以评估和改进证明工程。
论文指出，尽管测试与形式证明高度类比，变异分析在演绎验证中鲜有应用。作者提出 mutation proving，用于分析使用证明助手的验证项目，并在 Coq 上实现工具 mCoq。mCoq 借鉴函数式语言的变异算子，对 Coq 函数与数据类型定义进行变异，再检查受影响引理的证明是否仍然通过。为使技术实用，mCoq 实现了并行证明检查等优化。作者在多个中大型 Coq 项目上评估，记录不同变异算子下证明的通过/失败情况，并定性分析变异体，发现许多规约不完整的实例。评估过程中还改进了 Coq 文件序列化，并发现一个被开发者确认的 Coq 自身 bug。该工作可帮助证明工程师提升验证项目质量，也可供研究者评估证明工程技术。
Mutation analysis, which introduces artificial defects into software systems, is the basis of mutation testing, a technique widely applied to evaluate and enhance the quality of test suites. However, despite the deep analogy between tests and formal proofs, mutation analysis has seldom been considered in the context of deductive verification. We propose mutation proving, a technique for analyzing verification projects that use proof assistants. We implemented our technique for the Coq proof assistant in a tool dubbed mCoq. mCoq applies a set of mutation operators to Coq definitions of functions and datatypes, inspired by operators previously proposed for functional programming languages. mCoq then checks proofs of lemmas affected by operator application. To make our technique feasible in practice, we implemented several optimizations in mCoq such as parallel proof checking. We applied mCoq to several medium and large scale Coq projects, and recorded whether proofs passed or failed when applying different mutation operators. We then qualitatively analyzed the mutants, finding many instances of incomplete specifications. For our evaluation, we made several improvements to serialization of Coq files and even discovered a notable bug in Coq itself, all acknowledged by developers. We believe mCoq can be useful both to proof engineers for improving the quality of their verification projects and to researchers for evaluating proof engineering techniques.
DOI 原文 ·
@inproceedings{paperbot5303,
title = {Mutation Analysis for Coq},
author = {Ahmet Celik and Karl Palmskog and Marinela Parovic and Emilio Jesus Gallego Arias and Milos Gligoric},
booktitle = {ASE},
year = {2019},
doi = {10.1109/ase.2019.00057}
}