Vous êtes ici

CELTIQUE

Responsable: Thomas JENSEN

Certification de logiciel par analyse sémantique
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 certification de logiciel peut s'appuyer 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 certification 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 projet industriel pour le compte de la SGDN sur la construction d'une machine virtuelle JAVA sécurisée.

Créée le : 01/07/2009
Établissement de rattachement : Université de Rennes 1, Inria, INSA Rennes, ENS Rennes
Localisation : Rennes (35)