Projet ProVal
rapport d'avancement final

1  Composition de l'équipe

2  Avancement

• Gestion multi-prover des obligations de preuve : mise au point d'une interface graphique permettant de visualiser la résolution des obligations de preuve par différents outils; méthodes de traduction entre différents formalismes, élimination du polymorphisme ...
• Outil de résolution d'obligations de preuve Ergo un outil modulaire traitant une logique multi-sortée polymorphe
• Méthodes efficaces de génération d'obligations de preuve dans Why
• Modèle pour la gestion correcte des transactions dans JavaCard [1]
• Travail sur les invariants en liaison avec Grenoble
• Définition d'une extension de JML pour la prise en compte de modèles abstraits logiques

3  Perspectives

• Revoir l'architecture Caduceus/Why/Krakatoa afin de factoriser les analyses de la mémoire et la gestion des invariants entre les codes C et Java
• Poursuivre la réflexion sur les modèles abstraits et les invariants, proposer une implantation.

Références

[1]

Claude Marché and Nicolas Rousset. Verification of Java Card applets behavior with respect to transactions and card tears. In Dang Van Hung and Paritosh Pandya, editors, 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), Pune, India, September 2006.

Ce document a été traduit de L^AT_EX par H^EV^EA