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


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

Responsables : Ahmed Bouajjani (http://www.liafa.jussieu.fr/~abou), 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 la cas du logiciel TReX, développé à LIAFA (www.liafa.jussieu.fr/~sighirea/trex) qui utilisent pour le moment une représentation symbolique classique de ces contraintes (bibliothèque Foaf).
Des chercheurs belges ont développée une bibliothèque qui utilise une représentation plus compacte, sous forme d'automates, appelée NDD. Le travail proposé dans ce TER est d'étudier cette dernière bibliothèque et puis de implémenter une interface entre TReX et les NDD. Le langage de programmation seront le C ou le C++.

Connaissances préalables souhaitées : Resultats :