Résumé: L'utilisation des programmes informatiques dans des applications critiques nécessite l'utilisation des méthodes formelles basées sur la rigueur mathématique pour établir leur correction conformément à leurs spécifications. La méthode formelle Why permet de générer, à partir d'un programme C spécifié avec Caduceus, un ensemble d'obligations de preuves qu'il faut prouver à l'aide d'un assistant de preuve pour établir la correction du programme. Le calcul matriciel est intensivement utilisé dans les programmes scientifiques. Ceci a engendré le développement de plusieurs librairies dont BLAS (Basic Linear Algebra Subroutines), pour permettre une écriture rapide et efficace des programmes de calcul matriciel. Dans notre travail, nous avons utilisé la méthode Why pour prouver deux programmes issus des BLAS : le produit matriciel et la résolution des systèmes. Nous avons utilisé l'assistant de preuve Coq pour décharger les obligations de preuves. Pour mener les preuves, nous avons proposé une nouvelle définition du type matrice qui peut être utilisé pour prouver d'autres programmes.

Boumerdes:
Langue: Français
Collation: 103 p. ill. ;30 cm
Diplôme: Magister
Etablissement de soutenance: Boumerdes, Université de M'hamed Bougara. Faculté des Sciences
Spécialité: Système Informatique
Index décimal 621 .Physique appliquée (électrotechnique, génie civil, génie mécanique, ingénierie appliquée, principes physiques en ingénierie)
Thème Informatique

Mots clés:
Solveurs (logiciels)
Matrices
Logiciels

Note: Bibliogr.pp.98-103