On Construction of a Library of Formally Verified Low-level Arithmetic Functions, Innovations in Systems and Software Engineering, vol.9, pp.59-77, 2013. ,
Verification of Dependable Software using SPARK and Isabelle, 6th International Workshop on Systems Software Verification (OpenAccess Series in Informatics (OASIcs), vol.24, pp.15-31, 2012. ,
A Proof of GMP Square Root, Journal of Automated Reasoning, vol.29, pp.225-252, 2002. ,
URL : https://hal.archives-ouvertes.fr/inria-00101044
Why3: Shepherd Your Herd of Provers, Boogie 2011: First International Workshop on Intermediate Verification Languages, pp.53-64, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00790310
One Logic To Use Them All, 24th International Conference on Automated Deduction, vol.7898, pp.1-20, 2013. ,
The Spirit of Ghost Code, Formal Methods in System Design, vol.48, pp.152-174, 2016. ,
Why3 -Where Programs Meet Provers, 22nd European Symposium on Programming, vol.7792, pp.125-128, 2013. ,
Formal Verification of a Big Integer Library, DATE Workshop on Dependable Software Systems, 2008. ,
Assigning Meanings to Programs, Program Verification, pp.65-81, 1993. ,
A Why3 Framework for Reflection Proofs and its Application to GMP's Algorithms, 9th International Joint Conference on Automated Reasoning, vol.10900, pp.178-193, 2018. ,
Formal Verification of a State-of-the-Art Integer Square Root, IEEE 26th Symposium on Computer Arithmetic, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02092970
Improved Division by Invariant Integers, IEEE Trans. Comput, vol.60, pp.165-175, 2011. ,
Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code, 3rd International Conference on Certified Programs and Proofs, vol.8307, pp.66-81, 2013. ,
A Why3 Proof of GMP Algorithms, Journal of Formalized Reasoning, vol.12, pp.53-97, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02477578
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library, 9th Working Conference on Verified Software: Theories, Tools, and Experiments, vol.10712, pp.84-101, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01519732
A Verification Environment for Sequential Imperative Programs in Isabelle/HOL, International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp.398-414, 2005. ,
Verifying Branch-Free Assembly Code in Why3, Working Conference on Verified Software: Theories, Tools, and Experiments, pp.66-83, 2017. ,
HACL*: A Verified Modern Cryptographic Library. Cryptology ePrint Archive, 2017. ,