A Why3 proof of GMP algorithms

Reui-Helft, R

Reui-Helft, R (reprint author), TrustInSoft, Paris, France.; Reui-Helft, R (reprint author), INRIA, Rocquencourt, France.

JOURNAL OF FORMALIZED REASONING, 2019; 12 (1): 53

Abstract

Large-integer arithmetic algorithms are used in contexts where both their performance and their correctness are critical, such as cryptographic softwa......

Full Text Link