, Ensure: value(a, n) = value(s, n/2 + 1) 2 + value(r, result) Ensure: value(r, result) ? 2 × value(s, n) Ensure: result > 0 ? r
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, vol.24, pp.15-31, 2012. ,
A proof of GMP square root, Journal of Automated Reasoning, vol.29, issue.3-4, 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
Integer and polynomial multiplication: Towards optimal Toom-Cook matrices, 2007 International Symposium on Symbolic and Algebraic Computation, pp.17-24, 2007. ,
Modern Computer Arithmetic, 2010. ,
Preuves taillées en biseau, vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA), 2017. ,
On the minimum computation time of functions, 1966. ,
Certification of bounds on expressions involving rounded operators, Transactions on Mathematical Software, vol.37, issue.1, pp.1-20, 2010. ,
URL : https://hal.archives-ouvertes.fr/hal-00127769
A discipline of programming, vol.1, 1976. ,
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, issue.3, 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 Pragmatic Type System for Deductive Software Verification, 2016. ,
URL : https://hal.archives-ouvertes.fr/tel-01533090
An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969. ,
Multiplication of multidigit numbers on automata, Soviet Physics Doklady, vol.7, pp.595-596, 1963. ,
The Art of Computer Programming, Seminumerical Algorithms, vol.2, 1997. ,
A Why3 framework for reflection proofs and its application to GMP's algorithms, 9th International Joint Conference on Automated Reasoning, number 10900 in Lecture Notes in Computer Science, pp.178-193, 2018. ,
Formal verification of a state-of-theart integer square root, IEEE 26th Symposium on Computer Arithmetic (ARITH), 2019. ,
Improved division by invariant integers, IEEE Transactions on Computers, 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. ,
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. ,
The complexity of a scheme of functional elements realizing the multiplication of integers, Soviet Mathematics Doklady, vol.3, pp.714-716, 1963. ,
Hacker's Delight, 2012. ,
HACL*: A verified modern cryptographic library. Cryptology ePrint Archive, 2017. ,