, QuviQ testing tools, 2019.

J. Arndt, Matters Computational -Ideas, Algorithms, Source Code [The fxtbook, 2010.

F. Bobot, J. Filliâtre, C. Marché, G. Melquiond, and A. Paskevich, The Why3 Platform, 2018.
URL : https://hal.archives-ouvertes.fr/hal-00822856

L. Bulwahn, The new Quickcheck for Isabelle -Random, exhaustive and symbolic testing under one roof, CPP'12, vol.7679, pp.92-108, 2012.

S. Dailler, D. Hauzar, C. Marché, and Y. Moy, Instrumenting a weakest precondition calculus for counterexample generation, J. Log. Algebr. Meth. Program, vol.99, pp.97-113, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01802488

C. Dubois and A. Giorgetti, Tests and proofs for custom data generators. Formal Aspects of Computing, vol.30, pp.659-684, 2018.
URL : https://hal.archives-ouvertes.fr/hal-02302096

C. Dubois, A. Giorgetti, and R. Genestier, Tests and proofs for enumerative combinatorics, TAP'16, vol.6792, pp.57-75, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01670709

J. Filliâtre and M. Pereira, Itérer avec confiance, Journées Francophones des Langages Applicatifs (JFLA'16, 2016.

J. Filliâtre and M. Pereira, A modular way to reason about iteration, NFM'16, vol.9690, pp.322-336, 2016.

R. Genestier, A. Giorgetti, and G. Petiot, Sequential generation of structured arrays and its deductive verification, TAP'15, vol.9154, pp.109-128, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01228995

A. Giorgetti and R. Lazarini, Preuve de programmes d'énumération avec Why3, AFADL'18, pp.14-19, 2018.

A. Giorgetti, C. Dubois, and R. Lazarini, Combinatoire formelle avec Why3 et Coq, Journées Francophones des Langages Applicatifs (JFLA'19), pp.139-154, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02302086

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

C. Hri?cu, L. Lampropoulos, M. Dénès, and Z. Paraskevopoulou, QuickChick: Randomized property-based testing plugin for Coq, 2018.

D. Jackson and C. Damon, Elements of style: Analyzing a software design feature with a counterexample detector, IEEE Trans. Software Eng, vol.22, issue.7, pp.484-495, 1996.

K. R. Leino and M. Moskal, Usable auto-active verification, Usable Verification Workshop, 2010.

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

Z. Paraskevopoulou, C. Hri?cu, M. Dénès, L. Lampropoulos, and B. C. Pierce, Foundational property-based testing, ITP'15, vol.9236, pp.325-343, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01162898

R. Rieu-helft, C. Marché, and G. Melquiond, How to get an efficient yet verified arbitrary-precision integer library, VSTTE'17, vol.10712, pp.84-101, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01519732

C. Runciman, M. Naylor, and F. Lindblad, Smallcheck and lazy smallcheck: automatic exhaustive testing for small values, Proceedings of the 1st ACM SIG-PLAN Symposium on Haskell, pp.37-48, 2008.

K. J. Sullivan, J. Yang, D. Coppit, S. Khurshid, and D. Jackson, Software assurance by bounded exhaustive testing, Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, pp.133-142, 2004.