Vérification formelle d'extractions de racines entières

Yves Bertot 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : Nous décrivons la vérification formelle d'algorithmes de calcul de racines carrées, cubiques et énièmes dans un cadre fonctionnel. Nous montrons que les premiers algorithmes se décrivent bien en utilisant la représentation binaire des entiers, qui permet en outre d'assurer la terminaison de ces algorithmes. La même structure est sous-jacente à l'algorithme de racines énièmes, mais la terminaison de l'algorithme est vérifiée en utilisant des outils plus complexes. Le travail de vérification formelle a été effectué en utilisant le système Coq.
Mots-clés : Coq Vérification formelle de logiciels Calcul des constructions arithmétique des ordinateurs Coq.
Type de document :
Article dans une revue
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2005, Langages Applicatifs, Spécifications, Programmation, Vérification, 24 (9), pp.1161-1195
Liste complète des métadonnées
https://hal.inria.fr/inria-00001172
Contributeur : Yves Bertot <>
Soumis le : mardi 28 mars 2006 - 16:47:54
Dernière modification le : mercredi 12 septembre 2018 - 01:16:36
Document(s) archivé(s) le : samedi 3 avril 2010 - 21:16:31

Fichiers

racines.pdf

Identifiants

  • HAL Id : inria-00001172, version 1

Collections

INRIA

Citation

Yves Bertot. Vérification formelle d'extractions de racines entières. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2005, Langages Applicatifs, Spécifications, Programmation, Vérification, 24 (9), pp.1161-1195. 〈inria-00001172〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

206

Téléchargements de fichiers

345

Contact


archive-ouverte@inria.fr