Librairie OCAML pour le calcul des substitutions b et la génération des obligations de preuve
COLIN
Type de document
RAPPORT
Langue
francais
Auteur
COLIN
Résumé / Abstract
Utilisation d'une librairie logicielle de calcul sur les substitutions généralisées pour réaliser un générateur d'obligations de preuves pour spécifications formelles b. Ce développement utilise le langage fonctionnel OCAML (INRIA). (étude encadrée par G. Mariano -resp. INRETS ESTAS).
