Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __                                  
			  / _`  _   /  /  o           
			 /   ) __) /  /  / /  / /\/| 
			(___/ (_/ (_ (_ / (__/ /   |  
                                                
			  I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                           Lundi 1 décembre, 10h30

                               ---------------
                               Pierre Courtieu
                               ---------------

                                 CNAM & INRIA

              =================================================
              Travaux formels autour de la plateforme SPARK/Ada
              =================================================

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).

http://www.spark-2014.org/about