CELTIQUE

Semantic Analysis for Software Certification

Contexte et objectifs

Le programme de recherche de l’équipe Celtique vise à proposer des méthodes de certification sémantique de logiciels à l’aide d’analyse sémantique. Les techniques d’analyse sémantique permettent d’obtenir une description approchée du comportement d’un logiciel (valeurs et relations en tre entités numériques, flot de contrôle, état de la mémoire). La certificaiton de logiciel peut s’paauyer sur cette information, d’une part pour générer des données de test et d’autre part pour construire des certificats, prouvant formellement que le logiciel respecte une propriété donnée. Cela permet notamment de sécuriser le code mobile destiné à être télé-chargé sur des ordinateurs, des PDA, etc.

Axes de recherche

Analyse de programmes par interprétation abstraite.

Interaction entre analyse statique et procédures de décision.

Extraction de certificats de logiciels

Preuve formelles et certifification d’outils d’analyse sémantique

Relations internationales et industrielles

Participant au projet européen MOBIUS sur la sécurité de code mobile

Coordonnateur de plusieurs projets ANR (RAVAJ, CAVERN, DECERT) qui portent sur l’analyse et le test de logiciel

Participant à un projt indistriel pour le compte de la SGDN sur la construction d’une machine virtuelle JAVA sécurisée.

Dernière modification 15.06.2009 16h38

Responsable scientifique

Thomas Jensen
+33 2 99 84 74 78
Secrétariat +33 2 99 84 25 77

À propos de l'équipe

Site web
Rapport d'activité

Thème

Logiciel et architectures

Les projets du même thème

Adresse

IRISA - Campus universitaire de Beaulieu - 35042 Rennes Cedex

IRISA

Sections