Awesome

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.