Génération de code certifié pour des applications orientées objet spécification, raffinement, preuve et détection d'erreurs

L'objectif du projet est de proposer des méthodes et des outils pour le développement de programmes orientés objets offrant des garanties fortes de sécurité. Le projet s'intéresse plus spécifiquement à des programmes embarqués sur des cartes à puce ou dans des terminaux qui sont décrits dans des sous-ensembles de Java (par exemple JavaCard). Les travaux récents ont montré l'intérêt de spécifier des programmes Java à l'aide de formules exprimées dans le langage JML et la possibilité de construire des outils de vérification qui transforment un programme annoté en un ensemble d'obligations de preuve qu'il faut ensuite démontrer.

Activités de recherche
  Vérification
  Preuve de programme
  sécurité

Membres LRI


Pour en savoir plus : http://geccoo.lri.fr/