Tahina Ramananandro > Recherche >

Vérification formelle d'algorithmes probabilistes

J'ai effectué ce stage du 27 juin au 26 août 2005 à l'INRIA Sophia-Antipolis, au sein de l'équipe Marelle, sous la direction de MM. Philippe Audebaud et Laurent Théry, que je remercie ainsi que tous les membres des équipes Marelle ainsi que Everest.

L'équipe Marelle (Mathématiques, Raisonnement, Logiciel) s'occupe de la vérication formelle de logiciels, et travaille autour du système d'aide à la preuve Coq, tandis que l'équipe Everest (Environments for Verication and Security of Software), dans le même bâtiment, est spécialisée dans la vérication des aspects de sécurité des logiciels (notamment les protocoles cryptographiques).

Je dois dire que l'ambiance a été chaleureuse étant donné qu'à ma grande surprise, tout le monde se tutoie dans le laboratoire. J'ai pu avoir un aperçu signicatif du travail réalisé dans ces deux équipes en participant aux séminaires, aussi bien de cryptographie que de sémantique, organisés chaque jeudi après-midi

MM. les responsables de mon stage m'ont soutenu tout au long de mon expérience, tant sur le fond que du point de vue de la méthode de travail, tout en me laissant la liberté d'explorer le sujet par moi-même, liberté dont j'ai avantageusement profité pour aboutir à une présentation atypique selon leurs propres termes. Pour ce qui est de l'environnement de travail, j'ai commencé par une prise de contact avec le système d'aide à la preuve Coq, et j'avoue que j'y ai pris goût et c'est un doux euphémisme !

Vers la fin du stage, fin août, où il n'y a plus grand monde au laboratoire, pour cause de vacances, MM. Philippe Audebaud et Laurent Théry m'ont efficacement conseillé pour la réalisation du diaporama de l'exposé final, ainsi que pour la rédaction du rapport.

Fichiers du stage

Divers

Dernière modification le 18 septembre 2006