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

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

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.