Introduction

Software developed and verified using proof assistants, such as Coq, can provide trustworthiness beyond that of software developed using traditional programming languages and testing practices. However, guarantees from formal verification are only as good as the underlying definitions and specification properties. If properties are incomplete, flaws in definitions may not be captured during verification, which can lead to unexpected system behavior and failures. To address these problems, past research has commended mutation analysis, which is a general technique for evaluating specifications for adequacy and completeness, based on making small-scale changes to systems and observing the results.

We present mCoq, the first mutation analysis tool for Coq projects. mCoq changes Coq definitions, with each change producing a modified project version, called a mutant, whose proofs are exhaustively checked. If checking succeeds, i.e., the mutant is live, this may indicate specification incompleteness.

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.

Download

The latest release of mCoq is available on GitHub.

Resources

Publications

Kush Jain, Karl Palmskog, Ahmet Celik, Emilio Jesús Gallego Arias, and Milos Gligoric
mCoq: Mutation Analysis for Coq Verification Projects
International Conference on Software Engineering, Tool Demonstrations Track
(ICSE Demo 2020), to appear, Seoul, South Korea, May 2020.

Ahmet Celik, Karl Palmskog, Marinela Parovic, Emilio Jesús Gallego Arias, and Milos Gligoric
Mutation Analysis for Coq
International Conference on Automated Software Engineering
(ASE 2019), pages 539-551, San Diego, USA, November 2019.

Contributors

Contact

To report bugs or make feature requests, feel free to open a GitHub issue. You can also send comments or questions by email to any (or all) contributor(s).