La vérification de programmes impératifs est souvent longue et difficile tandis quelle est souvent plus facile pour les programmes fonctionnels purs (i.e. sans effet de bords). Cependant, les programmes fonctionnels ne sont pas toujours aussi efficaces que leurs homologues impératifs utilisant des pointeurs. Le but de ce stage était d'étudier la possibilité de générer des programmes impératifs efficaces à partir de programmes fonctionnels purs facilement vérifiables.
Ce rapport présente cette étude et une solution générant du code Scala à partir de code Isabelle utilisant des monades.
@TechReport{ Gi2008.2,
author = {Giorgino, Mathieu},
title = "{Vérification de structures de pointeurs}",
year = {2008},
month = {septembre},
type = {Rapport de Master},
institution = {Ecole Nationale Supérieure d'Electrotechnique, d'Electronique, d'Informatique, d'Hydraulique et des Télécommunications},
language = {français},
URL = {http://www.irit.fr/~Mathieu.Giorgino/Publications/pdfs/GiSt2009Generation_technique.pdf},
keywords = {Vérification de programmes impératifs et fonctionnels, programmation fonctionnelle, monades, Isabelle, Scala}
}