Mutation Analysis for Coq
Mutation Analysis for Coq
复制标题
DOI：
10.1109/ase.2019.00057
复制
发表时间：
2019-11
期刊：
影响因子：
--
通讯作者：
Ahmet Çelik;Karl Palmskog;Marinela Parovic;E. J. G. Arias;Miloš Gligorić
中科院分区：
文献类型：
--
作者：
Ahmet Çelik;Karl Palmskog;Marinela Parovic;E. J. G. Arias;Miloš Gligorić
突变分析将人为缺陷引入软件系统，是突变测试的基础，突变测试是一种广泛应用于评估和提高测试套件质量的技术。然而，尽管测试和形式证明之间存在深刻的相似性，但突变分析很少在演绎验证的背景下被考虑。我们提出了变异证明，这是一种使用证明助手来分析验证项目的技术。我们在名为 mCoq 的工具中实现了 Coq 证明助手的技术。受到之前为函数式编程语言提出的运算符的启发，mCoq 将一组变异运算符应用于 Coq 函数和数据类型的定义。 mCoq 然后检查受算子应用影响的引理证明。为了使我们的技术在实践中可行，我们在 mCoq 中实现了多项优化，例如并行证明检查。我们将 mCoq 应用于多个中型和大型 Coq 项目，并记录应用不同变异算子时证明是否通过或失败。然后我们对突变体进行了定性分析，发现了许多不完整规格的实例。在我们的评估中，我们对 Coq 文件的序列化进行了一些改进，甚至发现了 Coq 本身的一个显着错误，所有这些都得到了开发人员的承认。我们相信 mCoq 对于验证工程师提高验证项目的质量以及研究人员评估验证工程技术都非常有用。
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.