[hdrcouchot.git] / demandeInscription / synthese.tex

\documentclass[a4paper,french,11pt]{article}
%\usepackage{hyperlatex}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{framed}
\usepackage[amsmath,thmmarks,thref,framed]{ntheorem}
\usepackage[dvips]{graphics}
\usepackage{epsfig}
\usepackage{epsfig,psfrag}
\usepackage{subfigure}
\usepackage{color}
\usepackage{calc}
\usepackage{url}
\usepackage{longtable}
\usepackage{tabls}
\usepackage{textcomp}
%\usepackage{slashbox}
\usepackage{gastex}
\usepackage{pst-all}
%\input{format.sty}
\usepackage[frenchb]{babel}
\usepackage[a4paper]{geometry}
\input{symboles.sty}


\geometry{hmargin=1cm, vmargin=1.5cm }


\newcommand{\JFC}[1]{\begin{color}{green}\textit{#1}\end{color}}

%
%\lstset{% general command to set parameter(s)
%basicstyle=\small,          % print whole listing small
%keywordstyle=\color{black}\bfseries\underbar,
                                % underlined bold black keywords
%identifierstyle=,           % nothing happens
%commentstyle=\color{white}, % white comments
%stringstyle=\ttfamily,      % typewriter type for strings
%extendedchars = true,
%showstringspaces=false}     % no special string spaces



\usepackage{hyperref}
\pdfcompresslevel=9
\hypersetup{
     %backref=true,    %permet d'ajouter des liens dans...
     %pagebackref=true,%...les bibliographies
     %hyperindex=true, %ajoute des liens dans les index.
     colorlinks=true, %colorise les liens
     breaklinks=true, %permet le retour à la ligne dans les liens trop longs
     urlcolor= blue, %couleur des hyperliens
     linkcolor= blue, %couleur des liens internes
     %bookmarks=true, %créé des signets pour Acrobat
     bookmarksopen=true,            %si les signets Acrobat sont créés,
                                    %les afficher complÚtement.
     pdftitle={Demande d'inscription à l'HDR de JF COUCHOT}, %informations apparaissant dans
     pdfauthor={Jean-Fran\c{c}ois Couchot},     %dans les informations du document
     pdfsubject={Demande d'inscription à l'HDR de JF COUCHOT}          %sous Acrobat.
}




\makeindex

\newcommand{\inputladot}[2]{
\input{#1.dot.tex}
\includegraphics[width=#2]{#1.dot.ps}
}

\setcounter{secnumdepth}{4}

\renewcommand{\thesection}{\Roman{section}}
%\renewcommand{\thesubsection}{~~~~\arabic{subsection}}
%\renewcommand{\theparagraph}{~~~~~~~~\arabic{paragraph}}

\begin{document}


\title{Mémoire de synthèse des activités de recherche et d'encadrement.}
\author{Jean-Fran\c{c}ois {\sc Couchot}}


%\lstset{language=C}
\maketitle

\section{Curriculum vit{\ae} (1 page).}


\subsection{Contacts}
\begin{itemize}
\item \textbf{web~:} \url{http://members.femto-st.fr/jf-couchot/}
\item \textbf{courrier~:} 
\begin{minipage}[t]{10cm} FEMTO-ST, dpt DISC, IUT BM, 19 rue du maréchal Juin,  90000 Belfort
\end{minipage}
\item \textbf{mail~:} \url{couchot@femto-st.fr}
\item\textbf {tel~:}       (+33) (0)3 84 58 77 38
\item\textbf {gsm~:} (+33) (0)6 76 06 68 94 
\end{itemize}

\subsection{Diplômes universitaires}
\begin{itemize}
\item{\bf{91~:}} Baccalauréat série C mention AB, Besançon.
\item{\bf{95~:}} Maîtrise de mathématiques pures, Université de
  Franche-Comté (UFC).
\item{\bf{96~:}} 
CAPES de mathématiques, IUFM d'Auvergne.
\item{\bf{02~:}} 
Maîtrise d'informatique, mention B (UFC). 
\item{\bf{02~:}}
 DEA Informatique, option {\em Génie Logiciel} (UFC). Stage intitulé {\em Atteignabilité d'états et spécifications
logico-ensemblistes}. Major de Promotion, mention TB. 
\item{\bf{avril 06~:}}
 Doctorat en  informatique au Laboratoire d'Informatique 
de l'Université de Franche Comté (LIFC EA 4269), 
sur la {\em vérification d'invariants par superposition}, 
mention très honorable.
\end{itemize}


\subsection{Fonctions et expériences professionnelles}
\begin{itemize}
\item{\bf{95-00~:}} Enseignant en mathématiques dans le secondaire,
  successivement à Aurillac(15), Beaune(21), Belfort(90) et 
  Montbéliard(25).  
\item{\bf{sept. 00-06~:}} PrCe $71^{eme}$ section, Unité de Formation
  et de Recherche (UFR) Sciences du 
  Langage de l'Homme et de la Société (SLHS) à l'UFC. 
\item{\bf{sept. 06-07~:}} Post-doctorant INRIA (projet ProVal) sur le
  thème de l'intégration de preuves interactives dans des preuves
  automatiques (et vice-versa). %pour la vérification de programmes C embarqués.
\item{\bf{sept. 07-08~:}} PrCe $71^{eme}$ section, UFR SLHS à l'UFC. 
\item{\bf{sept. 08-\ldots~:}} Maître de Conférences $27^{eme}$ section, IUT de Belfort-Montbéliard, dpt. informatique (UFC). 
\item{\bf{sept. 10-14\ldots~:}} \'Elu au Conseil d'Institut de l'IUT de Belfort-Montbéliard. 
 \end{itemize}


\section{Nom et type de l'équipe de recherche.}

Je suis membre de l'équipe Algorithmique Numérique Distribuée (AND) du 
Département d'Informatique des Systèmes Complexes (DISC)
du laboratoire FEMTO-ST. 
Je relève de l'école doctorale 37 Sciences Pour l'Ingénieur et Microtechniques (SPIM) de l'UFC.

L'avis du directeur de l'équipe et du directeur de l'école doctorale est 
annexé à cette synthèse (section~\ref{sec:avis:directeur}).
\JFC{joindre l'avis de Raphaël, d'Olga de Nicolas et de PH. Lutz} 


\newpage
\section{Résumé de la thématique de la thèse d'université (1 page)}
On considère en entrée de la démarche une description
mathématique d'un programme: par exemple une fonction enrichie avec  
une  spécification du contexte dans lequel elle est invoquée (la pré-condition) et 
une spécification exprimant quelles  propriétés sont garanties en retour (la
post-condition). Lorsque pré-condition et post-condition sont équivalentes,
on parle d'invariant.
La thématique de \emph{vérification de programmes par preuve automatique} 
consiste à tout d'abord construire des formules mathématiques 
qui doivent être vraies si et seulement si 
la post-condition est établie par le programme sous hypothèse de pré-condition,
puis ensuite à 
décharger ces formules dans des prouveurs de théorèmes. 
Cette thématique est au c{\oe}ur des travaux de recherche effectués
pendant mon doctorat et le post-doctorat qui a suivi à à l'Inria.



Durant mon travail de thèse intitulée 
{\em vérification d'invariants par superposition}, 
j'ai proposé différentes traductions en logique équationnelle 
des obligations de preuve,  
dans l'objectif de faire converger
le plus rapidement possible un prouveur par superposition qui les décharge.
J'ai démontré la correction et la complétude partielle de la démarche et 
ai montré que la démarche supplante celles basées sur la  
logique WS1S et l'outil MONA. 

Lors de mon postdoc à l'INRIA, j'ai d'abord montré qu'il était possible
d'instancier des contre-exemple~\cite{BCDG07} et de voir 
si ceux-ci sont atteignables~\cite{CouchotD07IFM} lorsque 
l'obligation de preuve à vérifier n'est pas établie.
Ceci peut aider l'ingénieur à corriger ses modèles.
Je  me suis ensuite intéressé  à la
logique du premier ordre polymorphe. 
Dans ce but, j'ai présenté un réducteur de logique
polymorphe vers de la logique sans sorte et de la logique multi-sorte
du premier ordre, préservant la correction et la
complétude~\cite{couchot07cade}. 
Toujours pendant mon post-doctorat, face au problème d'explosion
combinatoire rencontré  
lors de déduction automatique, j'ai présenté une approche
de réduction de
formules~\cite{couchot07FTP, cgs09:ip} de type SMT-LIB
basée sur la sélection des hypothèses les plus  
pertinentes.   
L'approche a été implantée et validée sur un exemple industriel réel
de 5000 lignes de Code C annoté fourni par Dassault aviation.







\subsection*{Publications issues de ces recherches}
 
\begin{enumerate}

\item \label{cgs09:ip}[CGS09],
J.-F. Couchot and A. Giorgetti  and N. Stouls, 
{G}raph {B}ased {R}eduction of {P}rogram {V}erification {C}onditions.
In AFM'09, {A}utomated {F}ormal {M}ethods (colocated with {CAV}'09),
pages 40--47, Grenoble, 2009, {ACM Press}. 


\item\label{couchot07cade}[CL07]
J.-F. Couchot and S. Lescuyer.
Handling polymorphism in automated deduction.
In {\em 21th International Conference on Automated Deduction
  (CADE-21)}, volume 4603 of {\em LNCS (LNAI)}, pages 263--278, Bremen,
  Germany, July 2007.

\item\label{CouchotD07IFM}[CD07]
J.-F. Couchot and F. Dadeau.
Guiding the correction of parameterized specifications.
In {\em Integrated Formal Methods}, volume 4591 of {\em Lecture Notes
  in Computer Science}, pages 176--194, Oxford, UK, July
2007. Springer.

\item\label{CH07}[CH07]
J.-F. Couchot and T. Hubert.
A Graph-based Strategy for the Selection of Hypotheses.
In {\em FTP 2007 - International Workshop on First-Order Theorem
  Proving}, pages 63--76, Liverpool, UK, September 2007.


\item \label{BCDG07}[BCDG07]
F.~Bouquet, J.-F. Couchot, F.~Dadeau, and A.~Giorgetti.
Instantiation of parameterized data structures for model-based
  testing.
In {\em B'2007, the 7th Int. B Conference}, volume 4355 of {\em
  LNCS}, pages 96--110, Besancon, France, January 2007, Springer.  



\item\label{CGK05}[CGK05]
J.-F. Couchot, A.~Giorgetti, and N.~Kosmatov.
 A uniform deductive approach for parameterized protocol safety.
 {\em ASE '05: Proceedings of the 20th IEEE International
  Conference on Automated Software Engineering}. 
IEEE Computer Society, pages 364--367, novembre 2005.



\item\label{CDDGR03}[CDD$^{+}$03]
J.-F. Couchot, F.~Dadeau, D.~D\'{e}harbe, A.~Giorgetti, and S.~Ranise.
Proving and debugging set-based specifications.
{\em Electronic Notes in Theoretical Computer Science, proceedings
  of the Sixth Brazilian Workshop on Formal Methods (WMF'03)}, volume~95, pages
  189--208, mai 2004.

\item\label{CDGR03}[CDGR03] %(\textbf{part}~: 25\%)
J.-F. Couchot, D.~D\'{e}harbe, A.~Giorgetti, and S.~Ranise.
Scalable automated proving and debugging of set-based specifications.
{\em Journal of the Brazilian Computer Society}, 9(2):17--36,
  novembre 2003).



\item\label{CG04}[CG04]
J.-F. Couchot and A.~Giorgetti.
Analyse d'atteignabilit\'e d\'eductive.
{\em Congr\`es Approches Formelles dans
  l'Assistance au D\'eveloppement de Logiciels (AFADL'04)},  pages 269--283,
  juin 2004.
%VERIFIE

\end{enumerate}
















\newpage
\section{Exposé des recherches réalisées au cours de la période postdoctorale}
\JFC{chapeau à refaire}


\subsection{Convergence de systèmes  dynamiques discrets}

Un système dynamique discret (SDD) est une fonction $f$ 
du $n$-cube ($\{0,1\}^n$) dans lui même et un mode opératoire
(parallèle, unaire, généralisé) qui peut être itéré 
en synchrone ou en asynchrone.
Ils ont été étudiés à de maintes reprises~\cite{Rob95,Bah00,bcv02}.
Pour chacun de ces modes, il existe des critères  (suffisants) de convergence
globale ou locale, souvent basés sur le fait que  $f$ est  
est un opérateur contractant ans un espace.

Les modes  asynchrones ont une dynamique avec plus de liberté 
puisqu'ils autorisent chaque élément à modifier sa valeur avant 
de connaître les valeurs des autres éléments dont il dépend. 
Cependant, lorsque les calculs à effectuer sur certains n{\oe}uds
sont coûteux en temps et/ou que les temps de communication sont élevés,   
ces modes peuvent présenter une convergence plus rapide que le cas synchrone.  

Dans~\cite{BCVC10:ir}, j'ai formalisé le mode des 
\emph{itérations mixes} (introduit dans~\cite{abcvs05})
qui combine synchronisme et asynchronisme.
Intuitivement, les n{\oe}uds qui pourraient engendrer des cycles dans 
les itérations asynchrones sont regroupés dans une même classe. 
Les noeuds à l'intérieur celle-ci groupe seront itérés de manière 
synchrone et les itérations asynchrones sont conservées entre les groupes. 
Pour gommer les  différences entre les n{\oe}uds d'une même classe
lorsqu'ils  sont vus depuis des n{\oe}uds extérieurs, j'ai défini le 
mode des \emph{itérations mixes avec délais uniformes}.


Grâce à cette formalisation, j'ai pu énoncer puis démontrer un théorème 
établissant que pour des conditions classiques de convergence des itérations
synchrones d'une fonction $f$, les itérations mixes à délai uniforme
convergent aussi vers le même point fixe.


L'étude de convergence de SDD est simple à vérifier 
pratiquement pour le mode synchrone. Lorsqu'on introduit des stratégies 
pseudo périodiques pour les modes unaires et généralisées, le problème 
se complexifie. C'est pire encore lorsqu'on traite des itérations asynchrones 
et mixes prenant de plus en compte les délais. 
Des méthodes de simulation basées sur des stratégies et des délais générés aléatoirement ont déjà été présentées~\cite{BM99,bcv02}.
Cependant, comme ces implantations ne sont pas exhaustives, elles ne sont intéressantes que lorsqu'elles fournissent un contre-exemple. 
Lorsqu'elles exhibent une convergence,  
cela ne permet que donner une intuition de convergence, pas  une preuve.
Autant que je sache, aucune démarche de preuve formelle automatique 
de convergence n'avait jamais été établie. 


J'ai montré dans~\cite{Cou10:ir} comment  simuler 
des SDDs selon tous les modes pour établir 
formellement leur convergence (ou pas).
Cette simulation est basée sur l'outil SPIN de \emph{Model-Checking}
qui est une classe d'outils adressant le problème de vérifier automatiquement
qu'un modèle vérifie une propriété donnée. Pour traiter le problème d'explosion 
combinatoire, les outils de cette classe 
appliquent des méthodes d'ordre partiel, d'abstraction,
de quotientage selon une relation d'équivalence.

Pour cela, j'ai présenté pour cela une démarche de traduction d'un SDD  
dans PROMELA qui est le langage de SPIN.
J'ai énoncé puis prouvé ensuite la  correction et la complétude de la démarche
Des données pratiques comme la complexité et des synthèses d'expérimentation
ont aussi été fournies.



\subsection{Construction de fonctions chaotiques}
Pr. Christophe Guyeux de l'équipe AND a proposé dans sa thèse~\cite{guyeuxphd} 
une caractérisation des fonctions $f$ de $\{0,1\}^n$ dans lui même 
dont les itérations sont chaotiques selon Devanney dans certains mode: 
il est nécessaire et suffisant que son graphe des itérations soit
fortement connexe.  
J'ai proposé plusieurs méthodes de construction de 
fonctions ayant de tels graphes d'itérations~\cite{bcgr11:ip,chgw+14:onp}.

Dans la première~\cite{bcgr11:ip},
l'algorithme enlève des arcs et vérifie ensuite que  
la forte connexité est maintenue.
Même si cet algorithme retourne toujours des fonctions dont le graphe 
des itérations est fortement connexe, il n'en est pas pour autant efficace 
car il  nécessite une vérification à posteriori de la 
forte connexité sur le graphe entier composé de  $2^n$ sommets.
La seconde méthode propose une solution à ce problème en présentant
des conditions suffisantes sur un graphe à $n$ sommets
qui permettent d'obtenir des graphes d'itérations fortement connexes.
Ce théorème a aussi été prouvé dans~\cite{bcgr11:ip}
et des instanciations effectives 
ont été produites. 
Une troisième méthode~\cite{chgw+14:onp} s'appuie sur les codes 
de Gray, ou de manière équivalente sur les cycles hamiltoniens du graphe des
itérations: un cycle qui visite chaque n{\oe}ud exactement une fois est un  
\emph{cycle hamiltonien}.
La démarche consiste à enlever du graphe un de ses cycles hamiltoniens dont 
la démarche de génération est un problème connu. 

Ces méthodes ont permis d'étendre à l'infini la classe des fonctions 
dont les itérations sont chaotiques.


\subsection{Apprentissage par réseaux neuronaux}
Nous disposons grâce aux travaux présentés à la section précédente d'un grand
nombre de fonctions dont les itérations sont chaotiques.
Nous avons entrepris d'étudier ces itérations et plus particulièrement leur 
apprentissage par un réseau de neurones. 
J'ai notamment pu contribuer à montrer pratiquement qu'il
est très difficile (voir impossible) de les prédire 
à l'aide de tels outils d'intelligence artificielle~\cite{bcgs12:ij}.


Nous nous sommes attaqués à un problème physique d'optimisation de  
l'écoulement d'un flux d'air le long d'un véhicule. 
Ce flux peut être modifié si l'on active des injecteurs d'air placés 
par exemple sur le becquet du véhicule. 
Le flux d'air peut être modélisé à l'aide d'équations de Navier-Stokes
dont on ne connaît pas de méthode analytique de résolution. 
De plus, le nombre de Reynolds calculé dans cette situation fait apparaître 
que le régime est extrêmement turbulent, donc difficile à prévoir.
Nous avons souhaité 
continuer nos expériences d'apprentissage à l'aide 
de réseau de neurones dans ce contexte~\cite{cds12:ip,cds13:ij}.
 
Il est apparu comme judicieux de mémoriser les configurations
représentant l'état des actionneurs à l'aide de nombres binaires.
De plus les codes de Gray, dont deux mots adjacents ne diffèrent que d'un 
bit se sont présentés comme une des manière de mémoriser les sorties du 
réseau de neuronnes comme un seul nombre binaire.
Quand on sait que trouver un chemin hamiltonien (comme étudié dans la partie précédente) dans un
$n$-cube revient à trouver un code 
de Gray dans un mot de $n$-bits. Les compétences acquises lors du travail 
sur les chemins hamiltoniens ont ainsi pu être réutilisées et approfondies.
Les résultats pratiques quant à l'utilisation de ces codes ce sont cependant 
révélés comme moins pertinents que l'utilisation de $n$ sorties.

\subsection{Génération de nombres pseudo-aléatoires}

Au commencement de ce travail, notre équipe disposait d'un générateur de nombres 
pseudo-aléatoires (PRNG) 
basé sur une seule fonction dont nous avions prouvé la chaoticité 
des itérations, à savoir la négation booléenne vectorielle. Cependant pour 
réussir les tests statistiques dédiées aux PRNGs, il était nécessaire d'itérer 
un grand nombre (arbitraire) de fois cette fonction entre deux 
sorties. 

Avec la production d'une grande collection de fonctions à itérations chaotiques, 
j'ai proposé de répondre à la question suivante: comment engendrer des fonctions 
dont les itérations vont produire des nombres simulant correctement l'aléa.
J'ai d'abord caractérisé les fonctions dont les itérations produisent des nombres 
selon une distribution uniforme~\cite{bcgr11:ip}. Pour cela il a fallu réécrire
l'algorithme de génération comme une marche aléatoire dans une partie du $n$-cube,
de se ramener à une chaîne de Markov puis d'utiliser la théorie élaborée sur ce sujet 
pour conclure. Par la même occasion, nous avons démontré que certaines fonctions 
chaotiques ne peuvent pas produire un aléa suivant une distribution uniforme.
La sortie est biaisée.

J'ai proposé ensuite des méthodes permettant de trouver de telles 
fonctions en commençant par filtrer celles qui ne disposent pas 
de cette caractéristique parmi toutes les fonctions chaotiques qui peuvent 
être engendrées~\cite{bcgr11:ip}. J'ai démontré ensuite que supprimer 
un cycle hamiltonien dans un $n$-cube permettait d'engendrer directement 
des fonctions avec une telle caractéristique~\cite{chgw+14:oip}.
De plus, je me suis attaché à montrer l'importance 
de l'équilibrage du chemin hamiltonien à enlever. 

Les générateurs produits ont d'abord été évalués avec succès
ont confirmé la qualité de 
ceux-ci~\cite{bcgw11:ip,chgw+14:onp,chgw+14:oip} en se confrontant à 
des batteries de tests telles que Die-Hard, NIST, TestU01.

Plus récemment, nous avons entrepris de trouver des bornes du temps d'arrêt
d'obtention d'une distribution uniforme d'un générateur construit en enlevant un chemin hamiltonien équilibré dans un $n$-cube. Le travail est en cours de soumission
en journal international.



\subsection{Masquage d'information}

La propriété de transitivité des fonctions chaotiques implique que l'on peut 
atteindre tout point depuis le voisinage de n'importe quel point.
Lorsqu'on cherche à embarquer une marque dans un media, 
si l'on souhaite de plus que celle-ci soit robuste, \textit{i.e.},
ne puisse pas être enlevée facilement, il paraît naturel d'embarquer 
cette marque sur une grande partie du media. L'utilisation de fonctions chaotique
paraît alors judicieuse.

J'ai participé à la formalisation de la méthode de
marquage de médias~\cite{bcg11b:ip,bcg11:ij} et particularisé
ceci à des images numériques fournissant un 
nouveau contexte pour l'étude théorique et mathématique d'algorithmes de marquage.
La chaos-sécurité a été introduite comme une nouvelle propriété 
de tels algorithmes de marquage comme existe
déjà la ($\epsilon$-)stego-securité.
Nous avons de plus montré la robustesse d'un tel marquage dans les 
domaines fréquentiels usuel (DWT et  DCT domains).

Des instances de ces algorithmes ont été présentées en sélectionnant de manière 
pertinenente les fonctions à itérer soit pour garantir une robustesse 
élevée~\cite{bcfg12b:ip,bcfg+13:ip} soit pour masquer l'information dans le média 
et être le moins détectable possible~\cite{bcfg12a:ip}. 

D'autre méthodes de watermarking ont été investiguées 
particulièrement celles basées sur la Quantization Index Modulation (QIM), méthodes 
étant supposées comme les plus robustes. Mes principales contributions 
sur ce travail --en collaboration avec des membres de l'Université Antonine au Liban--,
ont été 
d'intégrer ceci à du marquage de document PDF puis de 
présenter ce problème comme un problème d'optimisation. 
Grâce à une telle présentation nous avons pu trouver les paramètre optimaux
des méthodes QIM assurant à la fois robustesse et indetectabilité.
Le travail est en cours de soumission en journal international.

Lorsque l'objectif visé est l'indétectabilité, on parle de \emph{stéganographie}.
Ce domaine a été adressé en critiquant notament les scenarios usuels d'évaluation
des algorithmes de steganographie. J'ai proposé un cadre complémentaire permettant 
d'apprécier ces schémas de masquage~\cite{fccg15:ip}.
J'ai deplus participé à l'élaboration de l'algorithme STABYLO~\cite{ccg15:ij}
qui est un schéma de
stéganographie basé l'enfouissement de l'information dans les contours 
d'une image. Ma contribution a principalement été la formalisation de l'algorithme, 
son étude de complexité. Grâce a l'optimisation de cette dernière,
nous avons  pu montrer 
que cet algorihtme présente un excellent compromis entre la  sécurité
fournie et sa complexité.  





\subsection{Application à la génomique}  

Core génome 



\subsection*{Publications issues de ces recherches}


\newpage
\section{Perspectives de recherche (1 à 2 pages maximum)}

\newpage
\section{Insertion dans l'équipe de recherche (3 pages maximum).} 
Rôle personnel joué dans l'animation de la recherche au
sein de cette (ces) équipe(s), sa gestion administrative et financière. Obtention et
gestion de contrats de recherche. Collaborations internationales et insertion dans un
réseau international. Organisation de manifestations scientifiques (colloques,
congrès, diffusion des résultats de la recherche en direction du public…) ;

\newpage
\section{Encadrement et co-encadrement d'étudiants (1 page)} (maîtrise, DEA, thèses d'Université,
stages d'ingénieurs…) pour des activités de recherche en indiquant de manière
explicite la part d’encadrement assurée par le candidat à l’HDR  ;

\newpage
\section{Participation éventuelle à des tâches administratives d'intérêt collectif (1 à 2 pages)},
à l'activité d'enseignement, ou expérience en entreprise ;


\newpage
\section{Liste des publications}
selon le plan suivant : Internationales avec comité de
lecture ; Nationales avec comité de lecture ; Didactiques et non référencées ;
Chapitres de livres et documents multi-médias ; Compte-rendu de colloques (avec
sélection sur résumés puis sans sélection sur résumés) ;
\newpage
\section{Liste des communications}
 selon le plan suivant : Conférences sur invitation
personnelle ; Communication à des colloques, avec sélection sur résumés ;
Internationaux ; Nationaux ; Communications diverses.

\section{Avis du directeur de l'Equipe}\label{sec:avis:directeur}

\bibliographystyle{alpha}
\bibliography{abbrev,biblioand}



\end{document}