PROPOSITION DE SUJET DE MEMOIRE : Année académique 2003-2004

Référence :	PYS-L-C08
Promoteur (s) :	Pierre-Yves Schobbens Co-promoteur : Emmanuel Dieul
Titre du mémoire :	Vérification d'algorithmes écrits en B
Description du sujet :	La méthode B est une méthode formelle de conception de logiciel, permettant d'écrire une spécification formelle cohérente et de produire du code respectant cette spécification. L'outil actuellement développé par Clearsy permet de prouver qu'une spécification est cohérente. Cette preuve est parfois faite automatiquement (cas simples) ou faite manuellement (cas un peu compliqués). Cette preuve manuelle peut être assez laborieuse, ce qui rend la preuve de cohérence beaucoup plus longue. Lorsque la specification n'est pas cohérente, la preuve est manuelle et impossible à faire, mais l'outil ne dit pas que cette preuve est impossible (indécidable). L'idée est donc d'utiliser l'analyse statique pour trouver un contre-exemple et montrer que la spécification n'est pas cohérente. Le but du mémoire est donc d'utiliser un outil de résolution de contraintes existant, programmé en Oz, et d'adapter cet outil à un sous-ensemble du langage B. Cet outil pourra servir dans le cadre du cours de programmation de 2e candi.
Cycle :	Licence
Nombre d'étudiants:	1
Lieu(x) de stage :	Namur ou Charleroi
Prérequis :	Logique du 1er ordre (théorie des ensembles, preuves).