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 :