Vérification formelle d'extractions de racines

Yves Bertot 1
1 LEMME - Software and mathematics
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 racine énième, 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.
Document type :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00070657
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 9:08:12 PM
Last modification on : Monday, September 3, 2018 - 10:56:02 AM
Long-term archiving on: Sunday, April 4, 2010 - 9:40:12 PM

Identifiers

  • HAL Id : inria-00070657, version 1

Collections

Citation

Yves Bertot. Vérification formelle d'extractions de racines. RR-5344, INRIA. 2004, pp.23. ⟨inria-00070657⟩

Share

Metrics

Record views

101

Files downloads

429