Génération de code certifié pour des applications orientées objet
Spécification, raffinement, preuve et détection d'erreurs
Generation of Certified Code for Object Oriented Applications
specification, refinement, proof and error detection


Présentation

Ce projet est financé dans le cadre des ACI Sécurité pour une durée de 3 ans (juillet 2003-juillet 2006).

Résumé-Summary

Partenaires

Proposition initiale

HTML-PDF-Publications des membres du projet
Références des méthodes et outils associés

Travaux réalisés

Outils

Outils réalisés dans le cadre du projet

Publications

Publications réalisées dans le cadre du projet

Réunions de travail

15 janvier 2007 Réunion finale INRIA, Orsay
12 juin 2006 Détails de la Réunion INRIA, Sophia-Antipolis
10 mars 2006 Détails de la Réunion LSR, Grenoble
25 octobre 2005 Détails de la Réunion LRI, Orsay
27-28 juin 2005 Détails de la Réunion Loria, Nancy
14 mars 2005 Détails de la Réunion LRI, Orsay
13-14 sept 2004 Détails de la Réunion LIFC, Besançon Localisation-Hotels
6-7 mai 2004 Détails de la Réunion INRIA, Sophia-Antipolis
23 janvier 2004 Détails de la Réunion LSR, Grenoble
8 septembre 2003 Détails de la Réunion de démarrage LRI, Orsay


Avancement des tâches

Rapport final (draft) (pdf)
  1. Equipe TFC, LIFC, Besançon
  2. Projet Cassis, LORIA& INRIA Lorraine, Nancy
  3. Projet Everest, INRIA Sophia-Antipolis
  4. Projet ProVal, LRI& INRIA Futurs, Orsay
  5. Equipe Vasco, LSR Grenoble
Rapport à mi-parcours (pdf) (ps)
  1. Spécifications de haut niveau
  2. Raffinement et programmation orientée objet
  3. Génération et résolution d'obligations de preuve
  4. Détection d'erreurs
Ce document a été traduit de LATEX par HEVEA