Sites Inria

Version française

Séminaire des équipes de recherche

Travaux formels autour de la plateforme SPARK/Ada

© INRIA Sophie Auvin - G comme Grille

  • Date : 1/12/2014
  • Place : Inria Paris-Rocquencourt - Amphi Alan Turing - Bâtiment 1- 10h30
  • Guest(s) : Pierre Courtieu

Dans l'équipe CPR du laboratoire Cédric nous travaillons actuellement sur différents sujets liés au langage SPARK (un sous-ensemble bien choisi de Ada) et à la plateforme du même nom (preuve de programme, analyse de flots etc).

Je présenterai une partie de ces travaux, plus précisément je parlerai de la sémantique formelle du langage que nous avons commencé à écrire en Coq et du prototype de frontend CompCert pour SPARK que nous avons démarré récemment.

J'insisterai sur les spécificités de SPARK/Ada (runtime check, procédures imbriquées récursives).

Keywords: Gallium Séminaire Travaux formels SPARK/Ada Plateforme

Top