A Proof of GMP Square Root

Yves Bertot 1 Nicolas Magaud Paul Zimmermann 2
2 SPACES - Solving problems through algebraic computation and efficient software
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present a formal proof (at the implementation level) of an efficient algorithm proposed by Paul Zimmermann \cite{Zimmermann2000} to compute square roots of arbitrary large integers. This program, which is part of the GNU Multiple Precision Arithmetic Library (GMP) is completely proven within the Coq system. Proofs are developed using the Correctness tool to deal with imperative features of the program. The formalization is rather large (more than 13000 lines) and requires some advanced techniques for proof management and reuse.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2002, 29 (3-4), pp.225--252. 〈10.1023/A:1021987403425〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00101044
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:55:00
Dernière modification le : lundi 3 septembre 2018 - 10:56:02

Lien texte intégral

Identifiants

Collections

Citation

Yves Bertot, Nicolas Magaud, Paul Zimmermann. A Proof of GMP Square Root. Journal of Automated Reasoning, Springer Verlag, 2002, 29 (3-4), pp.225--252. 〈10.1023/A:1021987403425〉. 〈inria-00101044〉

Partager

Métriques

Consultations de la notice

257