DSpace About DSpace Software
 

Depot Institutionnel de l'UMBB >
Thèses de Doctorat et Mémoires de Magister >
Informatique >
Magister >

Please use this identifier to cite or link to this item: http://dlibrary.univ-boumerdes.dz:8080/handle/123456789/898

Titre: Preuve en coq de propriétés de programmes numériques partant du code en C
Auteur(s): Lounas, Razika
Mots-clés: Matrices
Logiciels
Solveurs (logiciels)
Issue Date: 2009
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
Description: 103 p. , ill. , 30 cm
URI: http://dlibrary.univ-boumerdes.dz:8080/jspui/handle/123456789/898
Appears in Collections:Magister

Files in This Item:

File Description SizeFormat
Lounas, Razika magister.pdf1,14 MBAdobe PDFView/Open
View Statistics

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

 

Valid XHTML 1.0! DSpace Software Copyright © 2002-2010  Duraspace - Feedback