Accéder directement au contenu Accéder directement à la navigation
Rapport

A proof of GMP square root using the Coq assistant

Yves Bertot 1 Nicolas Magaud 1 Paul Zimmermann 2
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
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 in to compute square roots of arbitrarily large integers. This program, which is part of the GNU Multiple Precision Arithmetic Library (GMP), is completely proven within the 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 :
Rapport
Liste complète des métadonnées

https://hal.inria.fr/inria-00072113
Contributeur : Rapport de Recherche Inria <>
Soumis le : mardi 23 mai 2006 - 19:49:22
Dernière modification le : vendredi 26 février 2021 - 15:28:07
Archivage à long terme le : : dimanche 4 avril 2010 - 22:53:56

Fichiers

Identifiants

  • HAL Id : inria-00072113, version 1

Collections

Citation

Yves Bertot, Nicolas Magaud, Paul Zimmermann. A proof of GMP square root using the Coq assistant. [Research Report] RR-4475, INRIA. 2002. ⟨inria-00072113⟩

Partager

Métriques

Consultations de la notice

633

Téléchargements de fichiers

1608