ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 24/9 - 2005  - pp.1161-1185  - doi:10.3166/tsi.24.1161-1185
TITRE
Vérification formelle d'extractions de racines entières

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.


ABSTRACT
This paper describes the formal verification of algorithms to compute square roots, cubic roots, and nth roots in a functional framework. We show that the first algorithms are easily described by using the binary representation of integers, a solution that moreover makes it possible to ensure the termination of these algorithms. The same algorithm structure underlies the algorithm for nth roots, but ensuring that it terminates requires more complex tools. The formal verification work was done using the Coq system.


AUTEUR(S)
Yves BERTOT

MOTS-CLÉS
vérification formelle de logiciels, calcul des constructions, arithmétique des ordinateurs, Coq.

KEYWORDS
formal software verification, calculus of constructions, computer arithmetics, Coq.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (174 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier