M. Papadakis, M. Kintis, J. Zhang, Y. Jia, Y. L. Traon et al., Mutation testing advances: An analysis and survey, Advances in Computers, vol.112, pp.275-378, 2019.

X. Leroy, Formal verification of a realistic compiler, Commun. ACM, vol.52, issue.7, pp.107-115, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00415861

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock et al., seL4: Formal verification of an OS kernel, Symposium on Operating Systems Principles, pp.207-220, 2009.

D. Woos, J. R. Wilcox, S. Anton, Z. Tatlock, M. D. Ernst et al., Planning for change in a formal verification of the Raft consensus protocol, Certified Programs and Proofs, pp.154-165, 2016.

T. Ringer, K. Palmskog, I. Sergey, M. Gligoric, and Z. Tatlock, QED at large: A survey of engineering of formally verified software, Foundations and Trends in Programming Languages, vol.5, pp.102-281, 2019.

P. Fonseca, K. Zhang, X. Wang, and A. Krishnamurthy, An empirical study on the correctness of formally verified distributed systems, European Conference on Computer Systems, pp.328-343, 2017.

X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and understanding bugs in C compilers, Conference on Programming Language Design and Implementation, pp.283-294, 2011.

A. Groce, I. Ahmed, C. Jensen, P. E. Mckenney, and J. Holmes, How verified (or tested) is my code? Falsification-driven verification and testing, Automated Software Engineering, vol.25, issue.4, pp.917-960, 2018.

T. Ball and O. Kupferman, Vacuity in testing, Tests and Proofs, pp.4-17, 2008.

L. Lampropoulos and B. C. Pierce, QuickChick Interface, 2018.

D. Le, M. A. Alipour, R. Gopinath, and A. Groce, MuCheck: An extensible tool for mutation testing of Haskell programs, International Symposium on Software Testing and Analysis, pp.429-432, 2014.

Y. Cheng, M. Wang, Y. Xiong, D. Hao, and L. Zhang, Empirical evaluation of test coverage for functional programs, International Conference on Software Testing, Verification, and Validation, pp.255-265, 2016.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

C. Team, Coq manual: Syntax extensions and interpretation scopes, 2019.

, Coq manual: Utilities, 2019.

A. Celik, K. Palmskog, and M. Gligoric, iCoq: Regression proof selection for large-scale verification projects, International Conference on Automated Software Engineering, pp.171-182, 2017.

A. Groce, J. Holmes, D. Marinov, A. Shi, and L. Zhang, An extensible, regular-expression-based tool for multi-language mutant generation, International Conference on Software Engineering, pp.25-28, 2018.

E. J. Arias, SerAPI: Machine-Friendly, Data-Centric Serialization for Coq, MINES ParisTech, Tech. Rep, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01384408

J. Mccarthy, Recursive functions of symbolic expressions and their computation by machine, part I, Commun. ACM, vol.3, issue.4, pp.184-195, 1960.

E. J. Arias, Coq issue #9204, 2018.

E. Tassi, Coq pull request #9206, 2018.

L. Bulwahn, The new Quickcheck for Isabelle: Random, exhaustive and symbolic testing under one roof, Certified Programs and Proofs, pp.92-108, 2012.

A. Pacelet and Y. Bertot, coq-dpdgraph, 2019.

J. C. Blanchette and T. Nipkow, Nitpick: A counterexample generator for higher-order logic based on a relational model finder, International Conference on Interactive Theorem Proving, pp.131-146, 2010.

S. Cruanes and J. C. Blanchette, Extending Nunchaku to dependent type theory, International Workshop on Hammers for Type Theories, vol.210, pp.3-12, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01401696

Z. Paraskevopoulou, C. Hritçu, M. Dénès, L. Lampropoulos, and B. C. Pierce, Foundational property-based testing, International Conference on Interactive Theorem Proving, pp.325-343, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01162898

Z. Chen, L. O'connor, G. Keller, G. Klein, and G. Heiser, The Cogent case for property-based testing, Workshop on Programming Languages and Operating Systems, pp.1-7, 2017.

M. Johansson, Automated theory exploration for interactive theorem proving, International Conference on Interactive Theorem Proving, pp.1-11, 2017.

D. Delahaye, A tactic language for the system Coq, Logic for Programming and Automated Reasoning, pp.85-95, 2000.
URL : https://hal.archives-ouvertes.fr/hal-01125070

O. Labs and &. Ppx, , 2017.

E. J. Arias, B. Pin, and P. Jouvelot, jsCoq: Towards hybrid theorem proving interfaces, Workshop on User Interfaces for Theorem Provers, pp.15-27, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01425752

R. A. Demillo, R. J. Lipton, and F. G. Sayward, Hints on test data selection: Help for the practicing programmer, Computer, vol.11, issue.4, pp.34-41, 1978.

T. A. Budd, R. A. Demillo, R. J. Lipton, and F. G. Sayward, Theoretical and empirical studies on using program mutation to test the functional correctness of programs, Symposium on Principles of Programming Languages, pp.220-233, 1980.

Y. Jia and M. Harman, An analysis and survey of the development of mutation testing, Transactions on Software Engineering, vol.37, issue.5, pp.649-678, 2011.

R. Just, D. Jalali, L. Inozemtseva, M. D. Ernst, R. Holmes et al., Are mutants a valid substitute for real faults in software testing?, " in International Symposium on Foundations of Software Engineering, pp.654-665, 2014.

M. Papadakis, D. Shin, S. Yoo, and D. Bae, Are mutation scores correlated with real fault detection?: A large scale empirical study on the relationship between mutants and real faults, International Conference on Software Engineering, pp.537-548, 2018.

A. Chlipala, Ltac anti-patterns, 2019.

H. Coles, PIT mutation testing, 2010.

R. Just, The Major mutation framework: Efficient and scalable mutation analysis for Java, International Symposium on Software Testing and Analysis, pp.433-436, 2014.

R. Just, M. D. Ernst, and G. Fraser, Efficient mutation analysis by propagating and partitioning infected execution states, International Symposium on Software Testing and Analysis, pp.315-326, 2014.

R. Gopinath, I. Ahmed, M. A. Alipour, C. Jensen, and A. Groce, Mutation reduction strategies considered harmful, Transactions on Reliability, vol.66, issue.3, pp.854-874, 2017.

J. Zhang, L. Zhang, M. Harman, D. Hao, Y. Jia et al., Predictive mutation testing, Transactions on Software Engineering, 2018.

R. Gopinath, C. Jensen, and A. Groce, Topsy-Turvy: A smarter and faster parallelization of mutation analysis, International Conference on Software Engineering, pp.740-743, 2016.

B. Wang, Y. Xiong, Y. Shi, L. Zhang, and D. Hao, Faster mutation analysis via equivalence modulo states, International Symposium on Software Testing and Analysis, pp.295-306, 2017.

L. Chen and L. Zhang, Speeding up mutation testing via regression test selection: An extensive study, International Conference on Software Testing, Verification, and Validation, pp.58-69, 2018.

K. Palmskog, A. Celik, and M. Gligoric, piCoq: Parallel regression proving for large-scale verification projects, International Symposium on Software Testing and Analysis, pp.344-355, 2018.

Y. Jia and M. Harman, Constructing subtle faults using higher order mutation testing, International Working Conference on Source Code Analysis and Manipulation, pp.249-258, 2008.

E. J. Arias, SerAPI: The Coq Se(xp)rialized Protocol, 2019.

G. Gonthier and A. Mahboubi, An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, issue.2, pp.95-152, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00515548

J. Mendez, , 2019.

B. Barras, C. Tankink, and E. Tassi, Asynchronous processing of Coq documents: From the kernel up to the user interface, International Conference on Interactive Theorem Proving, pp.51-66, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01135919

L. De-moura, S. Kong, J. Avigad, F. Van-doorn, and J. Von-raumer, The Lean theorem prover (system description), International Conference on Automated Deduction, pp.378-388, 2015.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL -A Proof Assistant for Higher-Order Logic, 2002.

M. Papadakis, M. Delamaro, and Y. Le-traon, Mitigating the effects of equivalent mutants with mutant classification strategies, Science of Computer Programming, vol.95, pp.298-319, 2014.

C. Team, Coq manual: Conversion rules, 2019.

L. De-moura, J. Avigad, S. Kong, and C. Roux, Elaboration in dependent type theory, CoRR, 2015.

D. Le, M. A. Alipour, R. Gopinath, and A. Groce, Mutation testing of functional programming languages, 2014.

J. Duregård, Automating black-box property based testing, 2016.

R. Braquehais and C. Runciman, FitSpec: Refining property sets for functional testing, Haskell Symposium, pp.1-12, 2016.

A. Efremidis, J. Schmidt, S. Krings, and P. Körner, Measuring coverage of Prolog programs using mutation testing, Functional and Constraint Logic Programming, pp.39-55, 2019.

S. Berghofer and T. Nipkow, Random testing in Isabelle/HOL, International Conference on Software Engineering and Formal Methods, pp.230-239, 2004.