---

Projets PR - 2010-2011 - La page sera complétée si besoin.

Dates à retenir :

Choix des sujets vendredi 5 novembre

Remise de la liste des 2 articles complémentaires associés à l'étude bibliographique (par email à dubois@ensiie.fr)

Remise des fiches de lecture et du plan de la synthèse le 1er décembre

Prochaine Séance d'encadrement Etude biblio 8 décembre à partir de 9h sur RDV.

Exposés le 14 décembre

Entre temps : n'hésitez pas à me contacter (mail, visite dans mon bureau) ou à contacter les encadrants extérieurs (par mail ou RDV téléphonique éventuellement, à voir avec eux) pour les sujets concernés.

Remise du rapport relatif à l'étude bibliographique : au plus tard le 20 décembre à midi (dépot sur le site électronique de dépot (rapport + transparents de l'exposé au format pdf) avec le nom PR-biblio et à la scolarité (rapport uniquement avant les vacances ou au plus tard le lundi 3 janvier 10h))

Les sujets

• Vérification formelle de programmes C (projet encadré par les chargés du cours IAS - chercheurs du CEA)
  Etude bibliographique : Vérification formelle de programmes avec pointeurs
  Thierry Hubert and Claude Marché. Separation analysis for weakest Precondition-based verification. In Heap Analysis and Verification (HAV'07), pages 81-93 Ici
  R. Bornat. Proving Pointer Programs in Hoare Logic; in Backhouse & Oliviera (eds) MPC 2000; LNCS 1837; pages 102 - 126. Ici
  Réalisation : Preuves de fonctions C autour d'une structure de données qui reste à choisir (pile, file ou autre).
  Etudiants :
  
  • Vincent FROGER et Fabien RECCO
  • Virgile GIRAUD et Sébastien LOPEZ GARCIA



• Logique de Hoare pour langage de bas niveau (goto)
  Etude bibliographique :
  Ando Saabas, Tarmo Uustalu: A Compositional Natural Semantics and Hoare Logic for Low-Level Languages. Electr. Notes Theor. Comput. Sci. 156(1): 151-168 (2006)
  Ici
  George C. Necula: Proof-Carrying Code. POPL 1997: 106-119 Ici
  Réalisation : Vérification d'assertions pour des programmes avec goto
  Réalisation en Ocaml - correction en Coq (dépendra du degré d'avancement)
  Etudiants :
  • Josselin Allys et Pierre-François Carpentier
  • Alexis Leclerc et Mathieu Couespel


• Refactoring de programmes fonctionnels
  Etude bibliographique : Refactoring de programmes
  Nik Sultana, Simon J. Thompson: Mechanical verification of refactorings. PEPM 2008: 51-60 Ici
  Huiqing Li and Simon Thompson. Tool Support for Refactoring Functional Programs. In Partial Evaluation and Program Manipulation, San Francisco, California, USA, January 2008. Ici
  Christopher Brown, Simon J. Thompson: Clone detection and elimination for Haskell. PEPM 2010: 111-120 Ici
  Réalisation : implantation et vérification de méthodes de refactoring basée sur les types (Ocaml et Coq)
  Etudiants :
  • Jean-Christophe Dutoit et Célia Le Tonquesse
  • Thibaut Pasquiou et Yves-Stan Le Cornec


• Vérification d'un OS
  Etude bibliographique :
  Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an OS kernel Communications of the ACM, 53(6), 107 - 115, (June, 2010) Ici
  June Andronick, David Greenaway and Kevin Elphinstone Towards proving security in the presence of large untrusted components Proceedings of the 5th Workshop on Systems Software Verification, Vancouver, Canada, October, 2010 Ici
  Réalisation : Vérification de propriétés de sécurité. A compléter
  Etudiants :
  • Mathieu Even et Alexis Chatzipanayotis
  • Marie Evrard et Bescond Jacky


• Contrôle d'accès
  Etude bibliographique :
  Andrew Boyton A verified shared capability model Proceedings of the 4th Workshop on Systems Software Verification, Aachen, Germany, October, 2009 Ici
  J. MacLean. Reasoning about security models. In Proceedings of IEEE Symposium on Security and Privacy, pages 123 - 131. IEEE, Apr. 1987. Ici
  Réalisation : Vérification en Coq d'un système de capacités
  Etudiants : Thomas Fayolle et Inès Mabrouck



• L'environnement Focalize (ou Focal)
  Etude bibliographique : Présentation de l'atelier et de son langage de spécification
  P. Ayrault, M. Carlier, D. Delahaye, C. Dubois, D. Doligez, L. Habib, T. Hardin, M. Jaume, C. Morisset, F. Pessaux, R. Rioboo, P. Weis, Trusted Software within FoCaL, C&ESAR 2008 - Trusting Trusted Computing ?, Rennes, Décembre 2008. Ici
  P.Ayrault, T.Hardin and F.Pessaux, Development of a generic voter under Focal, Third International Conference on Tests and Proofs (TAP09), Zurich, July 2009. Ici
  Voir aussi la page de Focalize
  Réalisation : utilisation de Focalize pour spécifier et développer une application - utilisation de l'outil de preuve Zenon.
  l'application sera déterminée prochainement
  Etudiants : Qiusheng WANG et Jiaming CHEN


• Event B et l'atelier Rodin
  Etude bibliographique : Présentation de Event B - Différences avec la méthode B
  J.-R. Abrial. The Event-B Modelling Notation, October 2007 Ici
  Kriangsak Damchoom, Michael J. Butler, Jean-Raymond Abrial. Modelling and Proof of a Tree-Structured File System in Event-B and Rodin. ICFEM 2008: 25-44 Ici
  Voir aussi la page de Event-B
  Réalisation : utilisation de Event-B et Rodin pour spécifier et développer une application.
  l'application sera déterminée prochainement
  Etudiants :
  • François-Xavier CHASSAGNE et Fériel LAMROUS
  • Mahay PARENT et Vincent DELORME

Répartissez-vous par binôme (2 équipes par sujet au maximum)....