Détail d'une fiche   Version PDF

CERTILAB (SR0328GR)

Spécifications formelles, certification de logiciel

CERTILAB →  MIRHO (SR0360CR)


Statut: Terminée

Responsable : Joelle Despeyroux

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

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

Domaine : Génie logiciel et calcul symbolique
Thème : Sémantique et programmation

Période : 01/01/2001 -> 31/12/2001
Dates d'évaluation :

Etablissement(s) de rattachement : <sans>
Laboratoire(s) partenaire(s) : <sans UMR>

CRI : Centre Inria d'Université Côte d'Azur
Localisation : Centre Inria d'Université Côte d'Azur
Code structure Inria :

Numéro RNSR : 200121482A
N° de structure Inria: SR0328GR

Présentation

L'objectif de notre équipe est l'élaboration de méthodes formelles pour la production de logiciel sûr.

Les applications visées sont essentiellement les preuves de propriétés de langages de programmation (typiquement la preuve de correction d'un compilateur). L'approche suivie est celle de la théorie des types. Nos preuves sont réalisées en machine, avec comme système assistant à la preuve privilégié: le système Coq, développé par l'équipe Logical.


Axes de recherche

  • Méthodes. Élaboration de méthodes de formalisation des langages de programmation dans les théories typées existantes.

  • Théorie des types; récursion et induction pour les termes de type fonctionnel. Il s'agit ici de proposer de nouvelles théories typées facilitant les preuves formelles.

  • Spécification formelle des langages de programmation. Nous nous intéressons ici essentiellement aux langages concurrents et à objets.

Ces trois axes de recherche sont très reliés et se fertilisent mutuellement.


Relations industrielles et internationales

  • Participation au projet européen IST Types (Computer-Assisted Reasoning based on Type Theory). 34 sites, dont 5 sites industriels.