mCoq: Mutation Analysis for Coq
mCoq is a tool for mutation analysis of verification projects that use the Coq proof assistant.
mCoq applies a set of mutation operators to Coq definitions, generating modified versions, called mutants, of the project. If all proofs of a mutant are successfully checked, a mutant is declared live; otherwise it is declared killed. mCoq produces HTML reports pinpointing both live and killed mutants in the Coq code, where live mutants may indicate incomplete specifications. Our original research paper provides more information on the technique and optimizations that mCoq implements.
If you have used mCoq in a research project, please cite our tool paper in any related publications:
@inproceedings{JainETAL20mCoqTool,
author = {Jain, Kush and Palmskog, Karl and Celik, Ahmet and
Gallego Arias, Emilio Jes{\'u}s and Gligoric, Milos},
title = {{mCoq}: Mutation Analysis for {C}oq Verification Projects},
booktitle = {International Conference on Software Engineering,
Tool Demonstrations Track},
pages = {To appear},
year = {2020},
}Requirements
- OCaml 4.07.1
- Coq 8.10.2
- SerAPI 0.7.0
- Python 3
- JDK 8 (or later)
- Gradle 6
- Git
Installation
We strongly recommend installing the required versions of OCaml, Coq, and SerAPI via the OPAM package manager, version 2.0.5 or later.
To set up the OPAM-based OCaml environment, use:
opam switch create 4.07.1
opam switch 4.07.1
eval $(opam env)
Then, install Coq and SerAPI, pinning them to avoid unintended upgrades:
opam update
opam pin add coq 8.10.2
opam pin add coq-serapi 8.10.0+0.7.0
Next, clone the mCoq repository and enter the directory:
git clone https://github.com/EngineeringSoftware/mcoq.git
cd mcoq
The entry point for using mCoq is the mcoq.py script. To see
the available options, use:
./mcoq.py --help
The tool currently assumes that all project Coq source
files to be mutated are listed in the _CoqProject file
in a Coq project's root directory.
Before performing mutations, the script will automatically check
that all mCoq dependencies are present. To disable these checks,
pass the option --nocheck.
Usage example
To apply mCoq to StructTact
revision 82a85b7, run:
./mcoq.py --project StructTact --threads 2 --sha 82a85b7 \
--url https://github.com/uwplse/StructTact.git \
--buildcmd "./configure && make -j2" --qdir ".,StructTact"
After running this command, the HTML report is available in the
reports/results/StructTact directory. We also provide the corresponding report
for online viewing.
For large Coq projects, we recommend setting the --threads option
to at least the number of CPU cores in the machine, since mutation analysis
may otherwise take a very long time to complete.
Authors
- Ahmet Celik
- Emilio Jesús Gallego Arias
- Milos Gligoric
- Kush Jain
- Karl Palmskog
- Marinela Parovic
Acknowledgements
The mCoq developers thank Arthur Charguéraud, Georges Gonthier, Farah Hariri, Cătălin Hrițcu, Robbert Krebbers, Pengyu Nie, Zachary Tatlock, James R. Wilcox and Théo Zimmermann for their feedback on this work.