Vérification formelle d'extractions de racines entières - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques Année : 2005

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

Yves Bertot

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.
Fichier principal
Vignette du fichier
racines.pdf (228.89 Ko) Télécharger le fichier

Dates et versions

inria-00001172 , version 1 (28-03-2006)

Identifiants

  • HAL Id : inria-00001172 , version 1

Citer

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, 2005, Langages Applicatifs, Spécifications, Programmation, Vérification, 24 (9), pp.1161-1195. ⟨inria-00001172⟩

Collections

INRIA INRIA2
89 Consultations
376 Téléchargements

Partager

Gmail Facebook X LinkedIn More