|
1 | 1 | # mCoq: Mutation Analysis for Coq |
2 | 2 |
|
3 | 3 | mCoq is a tool for mutation analysis of verification projects that use the |
4 | | -[Coq proof assistant](https://coq.inria.fr). mCoq applies a set of mutation |
5 | | -operators to Coq definitions, with each application generating a modified |
6 | | -version, called a mutant, of the project. If all proofs of a mutant are |
7 | | -successfully checked, the mutant is declared live; otherwise it is declared |
8 | | -killed. mCoq produces HTML reports pinpointing both live and killed mutants, |
9 | | -where live mutants may indicate incomplete specifications. The |
10 | | -[research paper][ase-paper] provides more information on the technique |
11 | | -and optimizations that mCoq implements. |
| 4 | +[Coq proof assistant](https://coq.inria.fr). |
| 5 | + |
| 6 | +mCoq applies a set of mutation operators to Coq definitions, generating |
| 7 | +modified versions, called mutants, of the project. If all proofs of a |
| 8 | +mutant are successfully checked, a mutant is declared live; otherwise it |
| 9 | +is declared killed. mCoq produces HTML reports pinpointing both live and |
| 10 | +killed mutants in the Coq code, where live mutants may indicate |
| 11 | +incomplete specifications. The [research paper][ase-paper] provides more |
| 12 | +information on the technique and optimizations that mCoq implements. |
12 | 13 |
|
13 | 14 | Note to ICSE-Demo reviewers: we recently cleaned up the code and improved |
14 | 15 | our scripts for running the tool, so the steps shown in the paper submission |
@@ -56,7 +57,7 @@ the available options, use: |
56 | 57 | ``` |
57 | 58 |
|
58 | 59 | For example, to apply mCoq to [StructTact][structtact-repo] |
59 | | -revision [b95f041][structtact-revision], use: |
| 60 | +revision [`b95f041`][structtact-revision], use: |
60 | 61 | ``` |
61 | 62 | ./mcoq.py --project StructTact --sha b95f041 \ |
62 | 63 | --url https://github.com/uwplse/StructTact.git \ |
|
0 commit comments