-
Benoît Robillard.
Vérification formelle d'un algorithme d'allocation de registres.
Stage du master M2 Informatique, parcours RO (CNAM et Université Paris VI) et de 3e année de l'ENSIIE, mars à septembre 2007,
co-encadrement avec Éric Soutif (CNAM).
-
Sonia Ksouri.
Logique de séparation et logique du rely/guarantee,
Stage du master LS, Paris VI, avril à septembre 2007,
co-encadrement avec Marc Shapiro (LIP6 et INRIA).
-
Thomas Moniot.
Sémantique formelle d'un sous-ensemble réaliste du langage C.
Stage du Master MOPS de l'Université d'Évry et de 3e année de l'IIE,
avril à septembre 2006.
- Maxime Bargiel.
Étude et extension du procédé @L-is pour la
vérification et l'enrichissement automatiques de glossaires formels.
Stage de maîtrise de l'Université de Sherbrooke (M.Sc. Canada),
septembre à août 2007,
co-encadrement avec Marc Frappier (Université de Sherbrooke).
- Zaynah Dargaye.
Sémantique formelle et pré-compilation d'un sous-ensemble du langage C.
Stage du Master Parisien de Recherche en Informatique, mars à juillet 2005,
co-encadrement avec Xavier Leroy.
- Agnès Gonnet.
Validation de glossaires en Coq.
Stage du DESS Développement de Logiciels Sûrs, CNAM-Paris VI, mars à septembre 2005,
financé par la société Bfd, co-encadrement avec Philippe Michelin.
- François Armand.
Certification en Coq d'un compilateur.
Stage de 3e année de l'IIE, février à juin 2004, financé par l'ARC Concert.
- Mourad Naouari.
Rétro-conception de transactions de bases de données.
Stage du DEA d'informatique IIE-INT-Université d'Évry, février à juin 2004,
co-encadrement avec Régine Laleau (LACL).
- Thibaut Tourneur.
Analyses de flots de données certifiées en Coq.
Stage de 3e année de l'IIE, février à juin 2003.
- Nathalie Ly.
Spécification et implémentation de mécanismes de réutilisation de composants de spécifications.
Stage du DESS Développement de Logiciels Surs, CNAM-Paris VI, février à septembre 2003,
co-encadrement avec Régine Laleau (LACL).
- Frédéric Gervais.
Réutilisation de composants de spécifications en B.
Stage du DEA d'informatique IIE-INT-Université d'Évry, février à septembre 2002,
co-encadrement avec Régine Laleau (LACL).
- Audrey Moulin.
Automatisation de traitements de migration de données.
Stage de 3e année de l'IIE, janvier à juin 1998, financé par la société Stéria et co-encadré avec une personne de cette société.
- Romain Vassallo.
Ergonomie et évolution d'un outil de compréhension de programmes.
Stage de 3e année de l'IIE, janvier à juin 1995.
- Nathalie Dubois, Pousith Sayarath.
Aide à la compréhension et à la maintenance du logiciel: les pointeurs en spécialisation de
programmes.
Stages de 3e année de l'IIE, janvier à juin 1995.
- Frédéric Paumier, Hubert Parisot.
Calculs interprocéduraux pour la spécialisation de programmes Fortran.
Stages de 3e année de l'IIE, janvier à juin 1994, financés par EDF.
- Skander Korrab.
Représentation de programmes dans Centaur.
Stage de 3e année de l'IIE, janvier à septembre 1993, financé par EDF.