Proposition de Travaux d'Etude et de Recherche
Maîtrise 2002-2003


Sujet : Utilisation et interface avec une librairie de representation des contraintes lineaires par des automates (RVA)

Responsable : Mihaela Sighireanu ( http://www.liafa.jussieu.fr/~sighirea)

Nature du stage : Etude et Programmation en C++
Nombre d'étudiants dans le groupe : de 1 à 3.

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 utilisent pour le moment une représentation symbolique syntaxique de ces contraintes (bibliothèque Foaf).
Des chercheurs de l'Université de Liège ont développé une bibliothèque (appelée RVA) qui utilise une représentation basée sur les automates finis de contraintes linéaires entre variables entières et/ou réelles. Le travail proposé dans ce TER est d'étudier cette bibliothèque et d'implémenter une interface entre TReX et les RVA. Le langage de programmation sera le C++.

Connaissances préalables souhaitées :