, QuviQ testing tools, 2019.
Matters Computational -Ideas, Algorithms, Source Code [The fxtbook, 2010. ,
, The Why3 Platform, 2018.
URL : https://hal.archives-ouvertes.fr/hal-00822856
The new Quickcheck for Isabelle -Random, exhaustive and symbolic testing under one roof, CPP'12, vol.7679, pp.92-108, 2012. ,
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
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
Tests and proofs for enumerative combinatorics, TAP'16, vol.6792, pp.57-75, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01670709
Itérer avec confiance, Journées Francophones des Langages Applicatifs (JFLA'16, 2016. ,
A modular way to reason about iteration, NFM'16, vol.9690, pp.322-336, 2016. ,
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
Preuve de programmes d'énumération avec Why3, AFADL'18, pp.14-19, 2018. ,
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
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
, QuickChick: Randomized property-based testing plugin for Coq, 2018.
Elements of style: Analyzing a software design feature with a counterexample detector, IEEE Trans. Software Eng, vol.22, issue.7, pp.484-495, 1996. ,
Usable auto-active verification, Usable Verification Workshop, 2010. ,
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
Foundational property-based testing, ITP'15, vol.9236, pp.325-343, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01162898
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
Smallcheck and lazy smallcheck: automatic exhaustive testing for small values, Proceedings of the 1st ACM SIG-PLAN Symposium on Haskell, pp.37-48, 2008. ,
Software assurance by bounded exhaustive testing, Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, pp.133-142, 2004. ,