\section{Sujet \thesujet : AltaRica : sémantique formelle et
environnement de preuves}\refstepcounter{sujet}\label{temps}

\subsection*{Fiche signalétique}

\begin{tabular}{llll}
{\bf Responsable} & Antoine Rauzy & 05 56 84 60 83 & Antoine.Rauzy@labri.u-bordeaux.fr \\
{\bf Collaborateur} & Pierre Castéran & 05 56 84  & Pierre.Casteran@labri.u-bordeaux.fr\\
{\bf Equipe} & \multicolumn{3}{l}{MVTsi}\\
{\bf Titre} & \multicolumn{3}{l}{\begin{tabular}{p{4in}AltaRica : sémantique formelle et
environnement de preuves}.\end{tabular}}\\
{\bf Catégorie} & \multicolumn{3}{l}{Théorique et expérimentale}\\
{\bf Position/AltaRica} & \multicolumn{3}{l}{Langage et outils}\\
 & \multicolumn{3}{l}{Moyen et long termes}\\
{\bf Financement} & \multicolumn{3}{l}{Bourse de thèse MENRT}
\end{tabular}

\subsection*{Présentation du sujet}

\begin{description}
\item[Contexte] 

Comme tout langage, AltaRica nécessite une sémantique formelle avant
le développement d'outils fiables le manipulant.

Les expériences récentes en validation de systèmes critiques montrent
clairement qu'aucune technique seule n'est capable de satisfaire tous
les besoins de vérification.

Une technique prometteuse semble le couplage d'une part d'outils automatiques de
vérification dont la portée se limite à une certaine classe de
formules et à une taille limitée des systèmes; d'autre part d'outils
permettant de prouver par des moyens semi-automatiques des résultats
ne se conformant pas à ces limitations.

\item[Travail demandé]

Une description formelle et complète du langage AltaRica dans sa
version actuelle, cette sémantique devant permettre la construction
d'outils de démonstration pour les descriptions AltaRica.

Le travail devra s'intégrer dans l'outil de raisonnement sur les
systèmes de transitions actuellement développé au LaBRI (projet
Robusta).

La phase terminale devra, non seulement aboutir à des préconisations
pour le projet AltaRica; mais également à des recommandations d'ordre
méthodologiques pour ce nouvel outil.

\item[Environnement]

Le projet Robusta est développé depuis un an sur l'environnement de
démonstration Isabelle, dont la programmation se fait dans le langage
fonctionnel ML.

La thèse s'appuiera évidemment sur les exemples 
académiques, mais également sur plusieurs exemples de systèmes
industriels qui sont d'ores et déjà disponibles (au LaBRI) et font
l'objet de collaboration entre le LaBRI et divers partenaires
industriels (CEA, Aerospatiale).

\end{description}

