Français Anglais
Accueil Annuaire Plan du site
Production scientifique
Contrat de l'équipe Toccata
HISSEO

DIGITEO
Sept. 2008 - Août 2011

Equipe : Toccata
Responsable : BOLDO Sylvie

Gestionnaire : 
Organisme gérant : INRIA

HISSEO

Hisseo vise à réunir des chercheurs dont les spécialités sont soit la compilation (Gallium, INRIA Paris - Rocquencourt.), soit l'analyse statique de programmes (ProVal et CEA LIST). Son objectif est de combler un vide existant au niveau de l'analyse de codes utilisant des calculs en virgule flottante. Les applications visées sont de type programmes embarqués, requérant un très haut niveau de confiance, dans les domaines de l'avionique, le nucléaire, l'automobile, etc.
La sémantique précise définie par la norme IEEE754 n'est pas respectée en détail par les compilateurs. Pour cette raison il est difficile d'avoir une confiance absolue dans les résultats d'analyses faites au niveau du code source. Les directions de recherche proposées s'appuient soit sur la définition d'une sémantique formelle de la compilation des calculs flottants, soit sur l'analyse de l'assembleur généré par la compilation, dans lequel les choix pouvant s'écarter de la norme sont explicités.

Activités de recherche
  Preuve de programme
  Arithmétique flottante
  Formalisation et preuves de programmes numériques
  Formalisation de langages (de spécification et de programmation) dans les assistants de preuve
  Vérification déductive de programmes

Membres LRI
MARCHÉ Claude
BOLDO Sylvie
MELQUIOND Guillaume


Pour en savoir plus : http://hisseo.saclay.inria.fr/
Contrats
° SESAME DIGIPODS UPS
INTERACTION COLLABORATIVE à DISTANCE ENTRE PLATEFORMES DE VISUALISATION HéTéROGèNES
REGION IDF