2026
Functional Correctness of an Optimized Modular Inversion Algorithm
The notes provided in the original description by Pornin are expanded into a complete formal proof, which eventually relies on the collaboration of deductive program verification and interactive theorem proving through the use of the tools Rocq and Why3.
A. Mahboubi, Guillaume Melquiond, Pierre-Yves Strub et al.
· International Conference on... · 1 citation