F. Bobot, J. C. Filliâtre, C. Marché, and A. Paskevich, Let?s verify this with Why3, International Journal on Software Tools for Technology Transfer, vol.17, issue.6, pp.709-727, 2014.

S. Dailler, C. Marché, and Y. Moy, Lightweight Interactive Proving inside an Automatic Program Verifier, Electronic Proceedings in Theoretical Computer Science, vol.284, pp.1-15, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01936302

J. C. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code, Formal Methods in System Design, vol.48, issue.3, pp.152-174, 2016.

R. Santika, An Analysis of West Country Dialect Used by Hagrid in J.K. Rowling?s Harry Potter, NOBEL: Journal of Literature and Language Teaching, vol.7, issue.1, pp.25-35, 2016.

M. Huisman, R. Monti, M. Ulbrich, and A. Weigl, VerifyThis collaborative long term challenge: The PGP key server challenge manual, 2019.

S. F. Siegel, CIVL solutions to verifythis 2016 challenges, ACM SIGLOG News, vol.4, issue.2, pp.55-75, 2017.