Raphaël Rieu-Helft

A Why3 proof of GMP algorithms

2019 · HAL (Le Centre pour la Communication Scientifique Directe)

Large-integer arithmetic algorithms are used in contexts where both their performance and their correctness are critical, such as cryptographic software. The fastest algorithms are complex enough that formally verifying them is desirable but challenging. We …