Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Mutation Analysis for Coq

Abstract : 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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

Littérature citée [61 références]  Voir  Masquer  Télécharger

https://hal-mines-paristech.archives-ouvertes.fr/hal-02434236
Contributeur : Claire Medrala <>
Soumis le : jeudi 9 janvier 2020 - 18:20:33
Dernière modification le : mercredi 23 septembre 2020 - 04:25:28
Archivage à long terme le : : samedi 11 avril 2020 - 11:09:44

Fichier

A-720.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-02434236, version 1

Citation

Ahmet Celik, Karl Palmskog, Marinela Parovi, Emilio Jesús Gallego Arias, Milos Gligoric. Mutation Analysis for Coq. 34th International Conference on Automated Software Engineering (ASE 2019, Nov 2019, San Diego, United States. ⟨hal-02434236⟩

Partager

Métriques

Consultations de la notice

41

Téléchargements de fichiers

47