ملخص: 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:
لغة: فرنسية
الوصف المادي: 103 p. ill. ;30 cm
الشهادة: Magister
مؤسسة مناقشة الرسالة: Boumerdes, Université de M'hamed Bougara. Faculté des Sciences
تخصص: Système Informatique
الفهرس العشري 621 .الفيزياء التطبيقية (الهندسة الكهربائية ، الهندسة المدنية ، الهندسة الميكانيكية ، الهندسة التطبيقية ، المبادئ الفيزيائية في الهندسة)
الموضوع الإعلام الآلي

الكلمات الدالة:
Solveurs (logiciels)
Matrices
Logiciels

ملاحظة: Bibliogr.pp.98-103