Equipe de recherche CELTIQUE

Certification de logiciel par analyse sémantique

Présentation de l'équipe

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 industrielles et internationales

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.

Mots-clés : Sémantique Analyse statique Test Certification de logiciel

Equipes de recherche du même thème :

Siège et centres de recherche Inria

Accès direct

Social