%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{Contrats}

\noindent{\footnotesize \begin{tabular}{lp{.5cm}lllp{1cm}p{.5cm}p{.5cm}p{.5cm}}
\rotatebox{40}{Type} & \rotatebox{40}{Coordinateur} & \rotatebox{40}{Resp. scient.} & \rotatebox{40}{Nom} & \rotatebox{40}{Financeur} & \rotatebox{40}{Période} & \rotatebox{40}{Durée (mois)} & \rotatebox{40}{Budget global (K\texteuro)} & \rotatebox{40}{Part LIPN (K\texteuro)} \\
\acs{ANR} &  $\bullet$ & M. Mayero & CerPAN & \acs{MENESR} & 12/2005-12/2008 &
36 & 150 & 40 \\
Linkage Int. & & L. Petrucci & & \acs{ARC} & 01/2004-12/2004 & 12 &
6 & 3 \\
\acs{PAI} &  $\bullet$ & L. Petrucci & FAST & \acs{MAE} & 07/2004-06/2006 &
24 & 23 & 12 \\
Small grant & & L. Petrucci & & \acs{UniSA} & 09/2005-12/2005 &
4 & 6 & 0 
\end{tabular}}


\subsubsubsection{CerPAN}
\textit{Autres partenaires : \acs{Inria}-Rocquencourt, 
\acs{CEDRIC} (CNAM), \acs{LRI} (Univ. Paris 11)}	

CerPAN : {Certification de programmes d'analyse numérique} 
(\acs{ANR} programme blanc 2005)

Dans ce projet nous nous intéressons au développement et à la mise en 
application des méthodes permettant de démontrer formellement la correction de 
programmes issus du domaine de l'analyse numérique. Beaucoup de programmes 
critiques sont issus de ce domaine, mais les travaux traitant directement des 
applications des méthodes formelles aux programmes d'analyse numérique sont 
rares. La principale raison est l'utilisation intensive des nombres réels 
(à virgule flottante) dans les programmes numériques, alors que les méthodes 
formelles manipulent plutôt des nombres entiers, ou plus généralement des 
structures discrètes. Deux méthodes sont explorées dans ce projet, toutes deux 
étant vouées à être mises en pratique sur une étude de cas (gradient 
analytique). La première consiste à utiliser des outils de vérification de 
programmes (déjà existants) tels que Caduceus. La seconde consiste à effectuer 
la formalisation et la preuve du problème correspondant au programme ou à 
l'algorithme étudié, puis à en extraire (principe d'extraction de Coq) un 
programme qui sera, de fait, prouvé correct.

\subsubsubsection{\textsc{pai fast} \& \acs{ARC} Linkage international \& \acs{UniSA}
  small divisional grant}
\textit{Autres partenaires : \acs{UniSA} (University of South Australia),
University of Adelaide}

Ce projet, démarré avec un programme Linkage International de l'\acs{ARC} en
2004, poursuivi jusqu'en juin 2006 par un PAI FAST (French-Australian Science
and Technology programme) et complété par une bourse de l'University of South
Australia finançant quelques mois de travail d'un étudiant en thèse,
s'est intéressé aux techniques modulaires d'analyse
de réseaux de Petri. Il comportait quatre volets : l'analyse de réseaux
communiquant par partage de données (places), l'étude de systèmes temporisés,
la prise en compte des données et la mise en \oe uvre de ces techniques dans
des outils ainsi que des études de cas. Il a conduit à plusieurs
publications~:~\cite{CL-LP-STTT-06,JB-GG-LP-NJC-05,CL-LP-CPN-05,JB-GG-LP-MOMPES-05,CL-LP-ACSD04}.