mCoq 1.0: mutation analysis for Coq 8.10

Announcements
1

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.

For example, the following mCoq command analyzes StructTact revision 82a85b7:

./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.

Best regards,
Karl and all contributors to the project

3 Likes
2

Thanks for posting this — fun experiment!

Might be worth noting that QuickChick comes with reasonably nice support for a “manual” form of mutation testing, where mutants are explicitly marked by programmers rather than being generated automatically. This is described in the QuickChick book (volume f4 of the Software Foundations series). And we used a similar but slightly more automated form of mutation testing in a paper called “Testing Noninterference, Quickly.”

Benjamin

3

Thanks for flagging these up. We believe the mCoq and QuickChick mutation analysis approaches have (largely) complementary uses. Most directly, mCoq mutations are indeed much more blunt, i.e., not as easy to guide by the developer, but on the other hand don’t require annotations or decidable properties as in mutation testing. However, failing proofs (killed mutants in mCoq) don’t automatically mean that the associated properties are false, while QuickChick testing can establish this unambiguously. This is why we conceptually distinguish “mutation proving” from “mutation testing”.

The QuickChick book is cited in our paper linked above, and there is a short comparison akin to the above. However, we were not aware of the extent to which mutation testing was used in the “Testing Noninterference” paper until it was pointed out to us by Catalin Hritcu fall 2019. We aim to include a short comparison in an mCoq tool paper.

4

We now finished our mCoq tool paper (accepted to the ICSE 2020 Demo track), which provides a succinct 4-page introduction to installing and using mCoq: