Proposition de Travaux d'Etude et de Recherche
Maîtrise 2002-2003
Sujet :
Utilisation et interface avec la librairie GNU GMP pour l'arithmétique
en précision arbitraire
Responsables :
Mihaela Sighireanu (
http://www.liafa.jussieu.fr/~sighirea )
Nature du stage :
Etude et Programmation en C++
Nombre d'étudiants dans le groupe :
de 1 à 2.
Description du sujet :
La complexité croissante des logiciels ainsi que leur plus large utilisation
dans des équipements critiques (avions, trains, voitures,...) demandent
s'assurer du bon fonctionnement de ces logiciels. Pour cela, des techniques
de vérification automatique des programmes ont été développées ces derniers
années. Ces techniques consistent à explorer tous les exécutions possibles
des logiciels afin de contrôler que ses calculs ou réactions satisfont
certaines propriétés (p.e., absence de division par 0, valeurs des variables
dans certaines bornes).
Les logiciels qui implémentent ces techniques utilisent souvent une
représentation symbolique des contraintes sur les variables.
C'est le cas du logiciel TReX, développé au LIAFA
(
www.liafa.jussieu.fr/~sighirea/trex)
qui utilise une représentation symbolique syntaxique de ces
contraintes (bibliothèque Foaf).
Les nombres (entiers ou réels) qui apparaissent dans les contraintes peuvent
avoir des valeurs qui dépassent les domaines des entiers et
des flotants du C (resp. C++) donc les opérations arithmétiques peuvent être
fausses.
Il existe des librairies qui permettent d'étendre la précision des calculs et
de représentation pour les nombres. L'une d'elle, disponible en licence
GNU est GMP.
Le travail proposé dans ce TER est d'étudier cette bibliothèque
et puis de modifier la bibliothèque FOAF de TReX pour pouvoir représenter les
nombres en précision arbitraire.
Le langage de programmation sera le C++.
Connaissances préalables souhaitées :
- Programmation,
- Compilation (essentiellement l'analyse syntaxique).