Dear Coq users and developers,
We are happy to announce the release of mCoq 1.0 for Coq 8.10, available on GitHub:
mCoq is a tool for mutation analysis of verification projects. 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, the 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. The research paper, published in the proceedings of ASE 2019, provides more information on the technique, operators, and optimizations that mCoq implements.
./mcoq.py --project StructTact --threads 2 --sha 82a85b7 \ --url https://github.com/uwplse/StructTact.git \ --buildcmd "./configure && make -j2" --qdir ".,StructTact"
We provide the corresponding HTML report on all StructTact mutants for online viewing. Since mutation analysis is time-consuming, we strongly recommend users to set the
--threads option to at least the number of cores in their machine.
mCoq is provided under the open source Apache 2.0 license, so please don’t hesitate to report issues and contribute on GitHub.
Karl and all contributors to the project