Détail d'une fiche   Version PDF

CELTIQUE (SR0327HR)

Certification de logiciel par analyse sémantique

LANDE (SR0126ZR) →  CELTIQUE →  EPICURE (SR0922AR)


Statut: Terminée

Responsable : Thomas Jensen

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2024" : Aucun mot-clé.

Mots-clés de "B - Autres sciences et domaines d'application - 2024" : Aucun mot-clé.

Domaine : Algorithmique, programmation, logiciels et architectures
Thème : Preuves et vérification

Période : 01/07/2009 -> 31/05/2022
Dates d'évaluation : 22/03/2011 , 17/03/2015 , 20/03/2019

Etablissement(s) de rattachement : U. RENNES 1, ENS RENNES
Laboratoire(s) partenaire(s) : IRISA (UMR6074)

CRI : Centre Inria de l'Université de Rennes
Localisation : Centre Inria de l'Université de Rennes
Code structure Inria : 031082-1

Numéro RNSR : 200918993K
N° de structure Inria: SR0327HR

Présentation

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