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


Sujet : Programmation d'une bibliothèque de BDD et extension aux DDD

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

Nature du stage : Programmation en Java.

Nombre d'étudiants dans le groupe : Entre 2 (pour les BDD) et 4 (pour les BDD et DDD).

Description du sujet : Les BDD (Binary Decision Diagrams) permettent de représenter des fonctions booléennes de façon généralement plus efficace que les tables de vérité, tableaux de Karnaugh ou autres formes canoniques (``somme de produits'', etc.). Leur utilisation pour la vérification des circuits logiques est à présent largement répandue.
Dans la première partie du projet, il s'agit de programmer en Java une bibliothèque de BDD qui permet de construire, de manipuler et d'afficher de tels objets. Cette bibliothèque est complètement spécifiée dans le rapport [1] ci-dessous.
La deuxième partie du projet consiste à étendre la bibliothèque de BDD pour obtenir une bibliothèque de DDD (Difference Decision Diagrams). Les DDD sont utilisés actuellement pour la vérification de systèmes temporisés (voir l'article [3] ci-dessous). Connaissances préalables souhaitées : Bibliographie
  1. H. R. Andersen. An Introduction to Binary Decision Diagrams. Version of October 1997 with minor revisions April 1998. 36 pp. (http://www.it.edu/people/hra/notes-index.html)
  2. R.E. Bryant. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams, ACM Computing Surveys 24-3, September 1992.
  3. J. Myller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference Decision Diagrams. In proceedings Annual Conference of the European Association for Computer Science Logic (CSL), September 20-25 1999. Madrid, Spain.
Resultats :