version vendredi soir après quelques refs

[hdrcouchot.git] / demandeInscription / synthese.tex

diff --git a/demandeInscription/synthese.tex b/demandeInscription/synthese.tex
index a2761f211d2c05803889b6b23c1def2a40338c12..b6595846d67e65bf9871ae24cf0ddda2f786cb0a 100755 (executable)
--- a/demandeInscription/synthese.tex
+++ b/demandeInscription/synthese.tex
@@ -1,4 +1,4 @@
-\documentclass[a4paper,french,11pt]{article}
+\documentclass[a4paper,french,12pt]{article}

 %\usepackage{hyperlatex}
 \usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}
 %\usepackage{hyperlatex}
 \usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}


@@ -31,6 +31,7 @@
 
 
 \newcommand{\JFC}[1]{\begin{color}{green}\textit{#1}\end{color}}
 
 
 \newcommand{\JFC}[1]{\begin{color}{green}\textit{#1}\end{color}}

+\newcommand{\etalchar}[1]{$^{#1}$}

 
 %
 %\lstset{% general command to set parameter(s)
 
 %
 %\lstset{% general command to set parameter(s)


@@ -44,7 +45,6 @@
 %showstringspaces=false}     % no special string spaces
 
 
 %showstringspaces=false}     % no special string spaces
 
 

-

 \usepackage{hyperref}
 \pdfcompresslevel=9
 \hypersetup{
 \usepackage{hyperref}
 \pdfcompresslevel=9
 \hypersetup{


@@ -60,7 +60,7 @@
                                     %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
                                     %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={Algèbre et géométrie}          %sous Acrobat.
+     pdfsubject={Demande d'inscription à l'HDR de JF COUCHOT}          %sous Acrobat.

 }
 
 
 }
 
 


@@ -80,44 +80,45 @@
 %\renewcommand{\theparagraph}{~~~~~~~~\arabic{paragraph}}
 
 \begin{document}
 %\renewcommand{\theparagraph}{~~~~~~~~\arabic{paragraph}}
 
 \begin{document}

+\renewcommand{\refname}{ }

 
 

-
-\title{Mémoire de synthèse des activités de recherche et d'encadrement.}
+\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
 
 \author{Jean-Fran\c{c}ois {\sc Couchot}}
 
 
 %\lstset{language=C}
 \maketitle
 

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

 
 
 \subsection{Contacts}
 \begin{itemize}
 
 
 \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 
+\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}
 \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
+\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).
   Franche-Comté (UFC).

-\item{\bf{96~:}} 
+\item{\bf{96:}} 

 CAPES de mathématiques, IUFM d'Auvergne.
 CAPES de mathématiques, IUFM d'Auvergne.

-\item{\bf{02~:}} 
+\item{\bf{02:}} 

 Maîtrise d'informatique, mention B (UFC). 
 Maîtrise d'informatique, mention B (UFC). 

-\item{\bf{02~:}}
+\item{\bf{02:}}

  DEA Informatique, option {\em Génie Logiciel} (UFC). Stage intitulé {\em Atteignabilité d'états et spécifications
  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~:}}
+logico-ensemblistes}. Major de promotion, mention TB. 
+\item{\bf{avril 06:}}

  Doctorat en  informatique au Laboratoire d'Informatique 
  Doctorat en  informatique au Laboratoire d'Informatique 

-de l'Université de Franche Comté (LIFC EA 4269), 
+de l'Université de Franche Comté (devenu département DISC de FEMTO-ST), 

 sur la {\em vérification d'invariants par superposition}, 
 mention très honorable.
 \end{itemize}
 sur la {\em vérification d'invariants par superposition}, 
 mention très honorable.
 \end{itemize}


@@ -125,39 +126,44 @@ mention très honorable.
 
 \subsection{Fonctions et expériences professionnelles}
 \begin{itemize}
 
 \subsection{Fonctions et expériences professionnelles}
 \begin{itemize}

-\item{\bf{95-00~:}} Enseignant en mathématiques dans le secondaire,
+\item{\bf{95-00:}} Enseignant en mathématiques dans le secondaire,

   successivement à Aurillac(15), Beaune(21), Belfort(90) et 
   Montbéliard(25).  
   successivement à Aurillac(15), Beaune(21), Belfort(90) et 
   Montbéliard(25).  

-\item{\bf{sept. 00-06~:}} PrCe $71^{eme}$ section, Unité de Formation
+\item{\bf{sept. 00-06:}} PrCe $71^{ème}$ section, Unité de Formation

   et de Recherche (UFR) Sciences du 
   Langage de l'Homme et de la Société (SLHS) à l'UFC. 
   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
+\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.
   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. 
+\item{\bf{sept. 07-08:}} PrCe $71^{ème}$ section, UFR SLHS à l'UFC. 
+\item{\bf{sept. 08-\ldots:}} Maître de Conférences $27^{ème}$ section, IUT de Belfort-Montbéliard (IUT BM), au département d'informatique (UFC). 
+\item{\bf{nov. 10- nov. 14:}} \'Elu au Conseil d'Institut de l'IUT BM. 

  \end{itemize}
 
 
  \end{itemize}
 
 

-\section{Nom et type de l'équipe de recherche.}
+\newpage
+\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.
 
 
 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 Raphale, d'Olga de Nicolas et de PH. Lutz} 
+
+
+\subsection{Avis du directeur de l'équipe}\label{sec:avis:directeur:equipe}
+
+\subsection{Avis du directeur de recherche}\label{sec:avis:directeur:recherhce}
+
+\subsection{Avis du directeur de l'école doctorale}\label{sec:avis:directeur:spim}

 
 
 \newpage
 
 
 \newpage

-\section{Résumé de la thématique de la thèse d'université (1 page)}
+\section{Résumé de la thématique de la thèse d'université}

 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 
 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écfication exprimant quelles  propriétés sont garanties en retour (la
+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} 
 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} 


@@ -167,29 +173,119 @@ la post-condition est établie par le programme sous hypothèse de pré-conditio
 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
 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.
+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}, 
 
 
 
 Durant mon travail de thèse intitulée 
 {\em vérification d'invariants par superposition}, 

-j'ai proposé différentes traductions en logique équationnelle 
+j'ai proposé différentes traductions en logique équationnelle~\cite{cdgr03:ij,cddg+04:ip,cg04:np,couchot04:onp} 

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

+J'ai appliqué ceci à la  vérification de protocoles notamment d'exclusion
+mutuelle~\cite{CGK05} définis à l'aide de spécifications ensemblistes B~\cite{cdgr04:onp}.
+
+
+
+
+
+\subsection*{Publications issues de ces recherches}
+ 
+
+\begin{thebibliography}{9}
+\bibitem{CGK05}
+Jean-Fran\c{c}ois Couchot, Alain Giorgetti, and Nikolai Kosmatov.
+\newblock A uniform deductive approach for parameterized protocol safety.
+\newblock In David~F. Redmiles, Thomas Ellman, and Andrea Zisman, editors, {\em
+  ASE}, pages 364--367. ACM, 2005.
+
+
+\bibitem{cddg+04:ip}
+Jean-Fran\c{c}ois Couchot, Fr\'ed\'eric Dadeau, D.~D\'eharbe, Alain Giorgetti,
+  and S.~Ranise.
+\newblock Proving and debugging set-based specifications.
+\newblock In A.~Cavalcanti and P.~Machado, editors, {\em WMF'03 proceedings},
+  volume~95 of {\em ENTCS, Electronic Notes in Theoretical Computer Science},
+  pages 189--208, Campina Grande, Brazil, May 2004.
+
+\bibitem{cdgr03:ij}
+Jean-Fran\c{c}ois Couchot, D.~D\'eharbe, Alain Giorgetti, and S.~Ranise.
+\newblock Scalable automated proving and debugging of set-based specifications.
+\newblock {\em Journal of the Brazilian Computer Society (JBCS)}, 9(2):17--36,
+  November 2003.
+\newblock ISSN 0104-6500.
+
+\bibitem{cg04:np}
+Jean-Fran\c{c}ois Couchot and Alain Giorgetti.
+\newblock Analyse d'atteignabilit\'e d\'eductive.
+\newblock In Jacques Julliand, editor, {\em Congr\`es Approches Formelles dans
+  l'Assistance au D\'eveloppement de Logiciels, AFADL'04}, pages 269--283,
+  Besan\c{c}on, France, June 2004.
+
+\bibitem{cdgr04:onp}
+Jean-Fran\c{c}ois Couchot, D.~D\'eharbe, Alain Giorgetti, and S.~Ranise.
+\newblock {B}arvey: {V}\'erification automatique de consistance de machines
+  abstraites {B}.
+\newblock In Jacques Julliand, editor, {\em AFADL'04, Approches Formelles dans
+  l'Assistance au D\'eveloppement de Logiciels,} pages 369--372, Besan\c{c}on,
+  France, June 2004.
+\newblock Session outils.
+
+
+\bibitem{couchot04:onp}
+Jean-Fran\c{c}ois Couchot.
+\newblock V\'erification d'invariant par superposition.
+\newblock In {\em {MAJECSTIC}'04, {MA}nifestation de {JE}unes {C}hercheurs
+  {STIC}}, Calais, France, October 2004.
+\newblock Actes en ligne sur { t
+  http://lil.univ-littoral.fr/\~{}lewandowski/majecstic/programme.html}.
+
+
+\end{thebibliography}
+
+
+
+
+
+
+
+
+
+
+

 
 

-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 
+
+
+
+\newpage
+\section{Exposé des recherches réalisées au cours de la période postdoctorale}
+
+Entre avril 2006 et aujourd'hui, les recherches réalisées ont concerné plusieurs domaines synthétisés ci-après. Le premier travail (Sec.~\ref{sub:verif}) 
+est une suite directe des travaux de thèse. Suivent six sections
+(de la Sec.~\ref{sub:sdd} à la Sec.~\ref{sub:hash}) sur les systèmes 
+dynamiques discrets et leurs applications, thématique 
+pour laquelle j'ai été recruté dans l'équipe AND du département
+DISC. Enfin la section~\ref{sub:gen} présente comment je me suis investi dans 
+le  domaine de la bio-informatique à l'aide de compétences connexes.
+Ces travaux ont été valorisés par des publications dont les références sont données à la section~\ref{sec:publi} et synthéthisées à la figure~\ref{fig:bilan}
+en fin de document.
+
+\subsection{Vérification de programmes par 
+  preuve automatique}\label{sub:verif}
+
+Lors de mon post-doctorat à l'INRIA, j'ai d'abord montré qu'il était possible
+d'instancier des contre-exemples~\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
 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
+polymorphe vers de la logique sans sorte et de la logique multi-sortes

 du premier ordre, préservant la correction et la
 complétude~\cite{couchot07cade}. 
 Toujours pendant mon post-doctorat, face au problème d'explosion
 du premier ordre, préservant la correction et la
 complétude~\cite{couchot07cade}. 
 Toujours pendant mon post-doctorat, face au problème d'explosion


@@ -208,141 +304,1007 @@ de 5000 lignes de Code C annoté fourni par Dassault aviation.
 
 
 
 
 
 

-\subsection*{Publication issues de ces recherches}
+\subsection{Convergence de systèmes  dynamiques discrets}\label{sub:sdd}
+
+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 un opérateur contractant dans 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.  
+
+J'ai formalisé le mode des 
+\emph{itérations mixtes} (introduit par Pr. J. M.  Bahi en 2005 notamment)
+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 de celle-ci 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 mixtes avec délais uniformes}.
+J'ai pu ainsi é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 mixtes à délai uniforme
+convergent aussi vers le même point fixe.
+Ceci a été synthétisé dans~\cite{BCVC10:ir}. 
+
+
+L'étude de convergence de SDDs de modèles de petite taille 
+est simple à vérifier pratiquement pour le mode synchrone parallèle: 
+l'espace d'intérêt est fini.  
+C'est beaucoup plus complexe lorsqu'on traite des itérations
+unaires, voire généralisées
+asynchrones et mixtes 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 avaient déjà été présentées.
+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 de 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 démontré qu'on peut 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}.
+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.
+J'ai présenté pour cela une démarche de traduction d'un SDD  
+dans 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.
+Ceci a été synthétisé dans~\cite{Cou10:ir}
+
+
+\subsection{Construction de fonctions chaotiques}
+Je me suis intéressé ensuite à l'étude du problème dual 
+de l'étude de divergence d'un SDD.
+Le Pr. C. Guyeux de l'équipe AND a proposé dans sa thèse en 2010
+une caractérisation des fonctions $f$ de $\{0,1\}^n$ dans lui-même 
+dont les itérations sont chaotiques selon Devanney pour un  mode donné: 
+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 d'outils d'intelligence artificielle~\cite{bcgs12:ij}.
+
+
+Nous nous sommes attaqués parallèlement 
+à 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.
+ 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ères de mémoriser les sorties du 
+réseau de neurones comme un seul nombre binaire.
+Or 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 se sont cependant 
+révélés comme moins pertinents que l'utilisation de $n$ sorties.
+Ceci a été valorisé dans les publications~\cite{cds12:ip,cds13:ij}.
+
+\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és 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. 
+

  
  

-\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.  
+Les qualités statistiques des générateurs produits  
+ont été évalués avec succès~\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 
+en collaboration avec Pr. P.-C. Heam du DISC
+est en cours de soumission
+dans un  journal international.
+
+Enfin j'ai été sollicité pour encadrer une thèse sur l'implantation 
+de générateurs de nombre pseudo-aléatoires à bases d'itérations 
+chaotiques sur des circuits logiques 
+programmables. J'ai commencé ce travail en encadrant une étude exhaustive 
+de toutes les instances d'implantations de cette classe.
+Ce travail complet théorique et pratique est terminé aujourd'hui et 
+est en cours de soumission dans un journal international.
+
+
+
+
+
+
+\subsection{Masquage d'information}\label{sub:ih}
+
+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 média, 
+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 média. 
+L'utilisation de fonctions chaotiques
+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.
+Nous avons de plus montré la robustesse d'un tel marquage dans les 
+domaines fréquentiels usuels (DWT ou DCT).
+
+Des instances de ces algorithmes ont été présentées en sélectionnant de manière 
+pertinente 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é investies, 
+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 Dr R. Darazy de l'Université Antonine au Liban
+et en co-encadrant le stage de M2 de Ahmad Bittar--,
+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 indétectabilité.
+Le travail est en cours de soumission dans un  journal international.
+
+Lorsque l'objectif visé est l'indétectabilité, on parle de \emph{stéganographie}.
+Ce domaine a été adressé en critiquant notamment les scénarios usuels d'évaluation
+des algorithmes de stéganographie. J'ai proposé un cadre complémentaire permettant 
+d'évaluer ces schémas de masquage~\cite{fccg15:ip}.
+Ceci se réalise en co-encadrant le doctorat de Y. Fadil.
+
+J'ai de plus participé à l'élaboration de l'algorithme STABYLO~\cite{ccg15:ij}
+qui est un schéma de
+stéganographie basé sur l'enfouissement de l'information dans les contours 
+présents dans une image. 
+Ce travail est en collaboration avec Pr. R. Couturier.
+Mes contributions ont principalement été la formalisation de l'algorithme et 
+son étude de complexité. Grâce a l'optimisation de cette dernière,
+nous avons  pu montrer 
+que cet algorithme présente un excellent compromis entre sécurité
+fournie et complexité.  
+
+\subsection{Les fonctions de hachage}\label{sub:hash}
+Une fonction qui calcule une empreinte servant à identifier rapidement toute 
+donnée fournie en entrée est une fonction de hachage. On utilise ce genre
+de fonctions dès qu'on veut comparer des éléments de grande taille car il 
+suffit de comparer leurs empreintes (généralement de taille plus réduite).  
+Une telle fonction doit induire de grandes variations dans l'empreinte 
+lorsque l'entrée varie même très peu. C'est l'effet avalanche. Cette 
+condition fait penser à la forte sensibilité aux conditions initiales
+d'une fonction chaotique.
+
+Forts de nos compétences sur les fonctions dont les itérations sont 
+chaotiques, nous avons proposé de nouvelles fonctions de hachage.
+Celles-ci combinent des outils classiques utilisés dans les
+fonctions de hachage 
+usuelles et des itérations de systèmes dynamiques discrets étudiés 
+au préalable.
+Nous avons prouvé que ces fonctions sont résistantes à la 
+seconde pré-image. Leur complexité, polynomiale en la taille 
+du message et la taille de l'empreinte, a été évaluée et correspond
+à ce que l'on attend d'une telle fonction.
+Nous avons de plus vérifié statistiquement le critère d'avalanche.
+Ces résultats ont été valorisés dans les publications~\cite{bcg11:ip,bcg12:ij}.
+
+
+
+
+\subsection{Application à la génomique}\label{sub:gen}
+
+Ayant acquis des compétences sur certaines structures de mathématiques 
+discrètes (particulièrement théorie des graphes, 
+relations d'équivalence,\ldots), j'ai pu contribuer en bio-informatique
+en les réappliquant notamment.
+
+Une de mes premières pistes de travail a été de proposer une méthode automatique 
+de construction d'un ensemble de gènes communs (nommés core-génome) 
+à une famille de génomes.
+La méthode s'appuie sur la construction du graphe de  similarité
+entre les gènes quotienté selon une relation d'équivalence pour en
+réduire sa taille. Chaque gène est assimilé à son représentant de
+classe dans chaque génome. Le core-génome se déduit comme  l'intersection 
+de tous les génomes. Ceci a donné lieu aux 
+publications~\cite{acgs13:onp,akgcs+14:oip,acgm+14:ij}.
+
+L'approche précédente souffrait de n'engendrer que des core-génomes de (trop)
+petits cardinaux. J'ai contribué notamment 
+à l'amélioration de la méthode en proposant une étape d'optimisation issue 
+d'une adaptation discrète la méthode d'essaims particulaires~\cite{aagp+15:ip}.
+D'autres travaux (dont la première étape est cette construction de 
+core-génome) ont été ensuite réalisés, principalement dans le but de 
+construire des arbre phylogénétiques de qualité~\cite{agcs+15:ip,aangc+15:ip}.
+
+
+Tous ces travaux ont été réalisés en collaboration avec M. Salomon et en co-encadrant 
+le doctorat de B. Alkindy.

 
 
 
 
 
 

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

 
 

+\newpage
+\section{Perspectives de recherche}

 
 
 
 

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

 
 

+\subsection{Les codes de Gray}
+L'utilisation des codes de Gray dans une démarche d'apprentissage 
+(d'écoulement d'air ou  de fonctions chaotiques) ne s'est pas révélée comme 
+concluante. Dans chacun des cas, la distance de Hamming entre deux 
+configurations voisines peut être très petite tandis que le chemin (dans le 
+cycle  hamiltonien) qui les relie peut être long et ce même 
+pour des codes équilibrés.
+Je propose de travailler sur ce problème discret en mesurant la qualité 
+du code de Gray à l'aide d'une fonction basée sur la longueur des chemins
+(du cycle hamiltonien) entre les configurations voisines.
+Je pense ainsi réduire ce problème à un problème d'optimisation et dégager 
+une démarche de génération, comme je l'ai fait en bio-informatique.
+ 
+Jusqu'à présent, la production de codes de Gray équilibrés pour la génération 
+de nombres pseudo-aléatoires bute sur des problèmes d'explosion combinatoire:
+les seuls algorithmes connus répondant à ce problème nécessitent a priori
+plus de $10^{36}$ évaluations pour $n=8$. 
+Il n'est ainsi pas raisonnable de mettre en  
+pratique ce genre d'approche lorsque chacune de ces évaluations prend 1s.
+On peut peut-être
+se contenter de codes ``presque'' équilibrés , à défaut de pouvoir 
+trouver ceux qui seront équilibrés.
+Je propose d'investiguer  
+dans cette thématique en exploitant des approches itératives permettant 
+d'obtenir des optimums locaux et trouver ainsi des codes presque équilibrés.

 
 
 
 

-\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
+ 
+\subsection{Génération de nombres pseudo-aléatoires}
+
+La démarche actuelle de génération de nombres pseudo-aléatoires
+consiste à marcher dans une partie d'un $n$-cube en choisissant son chemin
+à l'aide d'un générateur fourni en entrée. Or ces générateurs sont tous des 
+fonctions de $\{0,1\}^n$ dans lui-même. Cette approche
+semble pouvoir se réécrire
+comme un produit synchrone de deux automates.
+L'intérêt d'une telle réécriture est qu'on pourrait exploiter 
+tous les résultats théoriques et pratiques déjà connus dans la communauté
+des automates. 
+Je pense investiguer cette voie pour améliorer notre approche, 
+s'affranchir, à terme, de tout autre générateur et améliorer la
+connaissance à ce sujet.
+Les propriété établies notamment sur les temps d'arrêt devraient être conservées.
+Il restera à le prouver.
+
+
+Jusqu'à présent, une seule expérimentation d'implantation de nos générateurs 
+sur des dispositifs physiques comme les FPGAs a été réalisée. Celle-ci 
+s'est faite automatiquement à l'aide de l'outil Matlab. Si le code engendré
+sur le circuit est bien une implantation fidèle à la spécification,
+il n'en est pas pour autant efficace: le nombre de bits générés par surface
+est plutôt faible. Nous allons exploiter les meilleures démarches mises en 
+exergue lors de la rédaction d'un état de l'art exhaustif sur les PRNGs 
+implantés sur FPGA pour produire du code optimisé. 
+Je prévois de réaliser ceci dans la thèse de M. Bakiri, en cours.
+
+Pour générer une fonction dont la matrice de Markov est doublement
+stochastique, nous avons proposé principalement deux méthodes 
+(génération puis test, suppression de chemin hamiltonien dans un $n$-cube).  
+Ces deux méthodes ne passent pas à l'échelle, même pour des $n$ de petite taille.
+Je pense attaquer ce problème algébriquement et en programmation logique avec 
+contraintes. Dans le premier cas, on peut remarquer qu'un matrice
+composée de $1$ uniquement 
+en $(i,i+1)$ est une réponse triviale au problème. Je pense continuer l'étude 
+de ce genre de matrices et proposer une méthode plus générale de génération.
+Je prévois de réaliser ce travail avec M. S. Contassot, Pr. à l'Université de Lorraine.
+Le département DISC et l'équipe VESONTIO 
+a de fortes compétences en programmation logique avec 
+contraintes. J'ai déjà démontré que ce problème peut être soluble par cette
+approche, sans avoir pour autant réussi à le faire.
+Je prévois des collaborations avec l'équipe VESONTIO du DISC sur ce sujet.
+
+
+Enfin, marcher dans une partie d'un $n$-cube est le modèle théorique que 
+nous avons établi pour notre classe de générateurs. On pourrait cependant 
+penser à ``sauter'' dans ce $n$-cube, c'est-à-dire modifier plusieurs bits 
+en une seule itération. J'ai commencé à étudier ce modèle avec les résultats
+pratiques suivants: le nombre d'itérations suffisant pour un mélange 
+correct est plus petit que celui obtenu en marchant. De plus,  
+il diminue à mesure que $n$ augmente ce qui n'est pas le cas en marchant.
+Pour l'instant, nous n'avons pas réussi à obtenir des bornes
+du temps d'arrêt. Je propose d'investiguer aussi dans cette direction.
+
+
+
+\subsection{Masquage d'information}
+
+Concernant le marquage de données, plusieurs approches duales cohabitent pour 
+établir ou non la sécurité d'un algorithme 
+de cette classe: les probabilistes (stego-securité par ex.), 
+les métriques (chaos-securité par ex.),
+les cryptographiques (mesure de fuite d'information).
+Notre approche n'a pas encore été évaluée selon cette dernière métrique, ce 
+que je propose de faire. 
+
+Concernant l'indétectabilité, je propose de travailler à la fois sur 
+la stéganographie et sur la stéganalyse.
+Nos expériences sur les schémas les plus efficaces de stéganographie 
+nous font penser qu'embarquer un message dans les contours comme cela l'a été fait pour 
+STABYLO est perfectible: on sait depuis qu'il existe des fonctions mathématiques 
+qui modélisent ces contours. Lorsqu'on modifie sans garde la valeur des bits de ces 
+contours,  la ``continuité'' des fonctions qui les modélisent peut être perdue et 
+le message peut s'en trouver détectable. Que je sache, aucune approche de stéganographie 
+basée sur la continuité des fonctions de contours n'a jamais été proposée. 
+Je propose donc d'investiguer dans cette voie.
+
+Les démarches de stéganalyse sont souvent composées de 2 étapes: 
+caractérisation puis classification. 
+On extrait au préalable une grande quantité des caractéristiques du média 
+puis on utilise une méthode de 
+classification basée sur celles-ci. La communauté voit souvent cette 
+seconde étape comme une boite noire et se concentre 
+sur la construction de l'ensemble des caractéristiques les plus discriminantes.
+Autant que je sache, les méthodes algébriques 
+de réduction de domaine (analyse par composant principaux, SVD) 
+ont rarement été utilisées comme une étape intermédiaire entre la caractérisation et 
+la classification. Ces méthodes ont déjà été 
+appliquées avec succès lorsqu'elles sont combinées avec des méthodes 
+d'apprentissage, par exemple dans de la reconnaissance faciale.
+Je propose d'étudier cette piste dans ce domaine. 
+Ceci se réalisera notamment au travers du doctorat de Y. Fadil.

 
 

-\end{enumerate}

 
 
 
 
 
 

+\newpage
+\section{Insertion dans l'équipe de recherche} 

 
 

+La thématique principale de ma thèse et du post-doctorat qui a suivi 
+était la vérification de programmes par preuve automatique, soit de 
+la logique informatique.
+Suite à mon recrutement dans l'équipe AND, mes recherches se sont réorientées
+autour des SDDs et donc de l'analyse numérique plus généralement.
+En plus des publications obtenues avec les membres de l'équipe AND, 
+ce qui suit récapitule quelques éléments permettant 
+d'apprécier mon insertion dans l'équipe AND

 
 
 
 
 
 
 
 

+J'ai monté une collaboration active avec l'Université Antonine au Liban. 
+J'y ai été invité en mai 2013. J'ai par la suite co-encadré trois stages de 
+Master 2 recherche avec des membres de cette université.
+J'ai un article en cours de soumission résumant un travail en collaboration 
+avec un ancien étudiant et un enseignant chercheur de cette université.

 
 

+Je suis membre du GDR codes et cryptographie. J'ai à ce titre 
+participé aux Journées Codes et Stéganographie en 2012 (Rennes) 
+où j'ai présenté le travail 
+de \og Steganography: secure and robust algorithms \fg{} et en 2013 (Paris).

 
 
 
 

+J'ai co-organisé avec J. Bahi et C. Guyeux 
+\og The First Workshop on Information Hiding Techniques 
+for Internet Anonymity and Privacy (IHTIAP) \fg{} à Venise en juin 2012.
+Le comité de programme était composé
+de 18 chercheurs internationaux (dont je faisais aussi partie). 
+Il s'est  déroulé sur 1 journée.

 
 
 
 

+J'ai fait partie des comités de programme de conférences 
+comme \og international conference on evolving internet \fg{} 
+(2012, 2013,2014 )\ldots 
+J'ai été session chair de \og international conference on evolving internet\fg{}
+en 2011 et  IHTIAP en 2012

 
 

+J'ai reviewé des articles pour les journaux internationaux 
+suivants: The computer Journal, Springer Multimedia Tool and application, 
+Springer Annals in Telecommunication\ldots

 
 
 
 

-\newpage
-\section{Exposé des recherches réalisées au cours de la période postdoctorale (5 pages maximum)}
+Je suis régulièrement membre de jury des épreuves TIPE, épreuves communes
+à 90 concours d'ingénieurs (sessions 2012 et  2015) et fournis  
+à chaque session des sujets scientifiques pour l'épreuve.

 
 

-(ou post-DEA pour les candidats autorisés à présenter leur demande sans
-thèse), en identifiant les grandes thématiques de recherche, la démarche suivie et les
-retombées en terme de publications et/ou de brevets ;

 
 

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

 
 \newpage
 
 \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…) ;
+\section{Encadrement et co-encadrement d'étudiants} 

 
 

-\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  ;
+\subsection{Thèse d'université}
+
+Je co-encadre (à hauteur de 40\%) avec Michel Salomon (40\%) et  
+Jacques M. Bahi  (20\%) le doctorat de Bassam Alkindy
+sur les combinaisons d'approches pour la prédiction de l'évolution génomique.       
+Le doctorat a commencé en septembre 2012 et devrait être soutenu en 
+novembre 2015. 
+Ce travail de thèse a donné lieu à 6 publications dans des conférences 
+internationales.
+
+
+Je co-encadre (à hauteur de 50\%) avec Christophe Guyeux (50\%)
+le doctorat de  Youssra Fadil
+sur
+l'étude du comportement des outils d'intelligence artificielle
+face à des dynamiques complexes.      
+Le doctorat a commencé en décembre 2013 et devrait être soutenu en 
+décembre 2016.        
+Ce travail de thèse a donné lieu à 1 publication dans une conférence
+internationale.
+               
+
+Je co-encadre (à hauteur de 50\%) avec Christophe Guyeux (50\%)
+le doctorat de  Mohamed Bakiri
+sur
+l'implémentation matérielle de générateurs de nombres pseudo-aléatoires basés sur les itérations chaotiques.
+Le doctorat a commencé en septembre 2014 et devrait être soutenu en 
+aout 2017.     
+Ce travail de thèse a donné lieu à 1 publication dans un journal international 
+en cours de soumission.
+
+\subsection{Master 2 recherche}
+
+
+J'ai co-encadré (à hauteur de 34\%) avec Raphael Couturier (33\%) et 
+Rony Darazi -- Université Antonine au Liban--(33\%)
+le stage de recherche de Master 2 de  Ahmad Bittar
+sur
+la 
+Steganography in PDF documents based on Unprintable Control ASCII Codes.
+Le stage a commencé le 01 mai 2013 et a été soutenu le 30 septembre 2013. 
+Ce travail de Master a donné lieu à 1 publication dans un journal international 
+en cours de soumission (en révision mineure).
+
+
+
+
+J'ai co-encadré (à hauteur de 80\%) avec   
+Talar Atechian -- Université Antonine au Liban--(20\%)
+le stage de recherche de Master 2 de Hussein Nasser
+sur
+une  
+Critical Analysis of Distributed Algorithm for Sensor
+Network Lifetime Maximization.
+Le stage a commencé le 01 avril 2014 et a été soutenu le 31 août 2014. 
+
+
+Je co-encadre (à hauteur de 80\%) avec   
+Talar Atechian -- Université Antonine au Liban--(20\%)
+le stage de recherche de Master 2 de Khaled Daher 
+sur la désynchronisation du calcul d'optimisation de la durée de vie 
+d'un réseau de capteurs.
+Le stage a commencé le 01 avril 2015 et sera soutenu le 31 août 2015. 

 
 

-\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
 
 
 \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) ;
+\section{Participation à des tâches d'intérêt collectif}
+
+Depuis septembre 2000, je suis titulaire à l'Université de Franche-Comté,
+soit sur un poste de PrCe (de 2000 à 2008, sauf l'année 2006-2007) soit sur
+un poste de MdC. J'ai assuré un grand nombre d'enseignements de la première
+année de licence ou de DUT jusqu'en seconde année de Master. 
+Depuis mon
+recrutement comme MdC, j'ai recentré mes enseignements autour 
+de mes thématiques de recherche, à savoir essentiellement les 
+mathématiques discrètes.
+La répartition moyenne de mes enseignements 
+sur les quatre dernières années  est la suivante:
+\begin{itemize}
+\item 6\% en le master Informatique Mobile et Répartie (UFR STGI), 
+  dans l'UE de
+  \og Modélisation et d'Evaluation des Systèmes Informatiques \fg{};
+\item 7\% en Licence Pro Conception des Application Multi-tiers (LP CAM) à l'IUT BM dans l'UE de \og Développement d'applications mobiles\fg{};
+\item 15\% en encadrement de projets tutorés ou de stage;
+\item 28\% en DUT d'informatique  dans l'UE de 
+\og conception et développement d'applications mobiles\fg{}; 
+\item 44\% en DUT d'informatique  dans les UEs de 
+\og mathématiques discrètes \fg{} et 
+de
+\og  modélisations mathématiques \fg{}.
+\end{itemize}
+
+J'ai aussi la responsabilité de toutes les UE données ci-dessus et 
+suis de plus le coordinateur des enseignements de mathématiques 
+au département d'informatique de l'IUT BM. 
+Depuis septembre 2014, je suis le responsable du parcours TeProw
+de la LP CAM  localisée 
+à l'IUT BM. Cette licence 
+a aussi un parcours à l'UFR ST. Je coordonne toute l'organisation 
+de cette licence avec mon collègue de Besançon. 
+
+
+J'ai été membre élu du conseil d'institut de l'IUT BM 
+de novembre 2010 à novembre 2014. A ce titre j'ai participé à la vie administrative de l'IUT, 
+aux commissions de recrutement d'enseignants et  d'enseignants-chercheurs\ldots
+Depuis septembre 2014,  je suis élu au conseil du département d'informatique 
+de l'IUT BM. 
+
+
+
+
+

 \newpage
 \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{Publications après la thèse}\label{sec:publi}
+
+\subsection{Journaux internationaux avec comité de sélection}
+
+\begin{thebibliography}{CHG{\etalchar{+}}14b}
+
+\makeatletter
+\addtocounter{\@listctr}{6}
+\makeatother
+
+\bibitem{bcg12:ij}
+Jacques Bahi, Jean-Fran\c{c}ois Couchot, and Christophe Guyeux.
+\newblock Quality analysis of a chaotic proven keyed hash function.
+\newblock {\em International Journal On Advances in Internet Technology},
+  5(1):26--33, 2012.
+
+
+\bibitem{bcg11:ij}
+Jacques Bahi, Jean-Fran\c{c}ois Couchot, and Christophe Guyeux.
+\newblock Steganography: a class of secure and robust algorithms.
+\newblock {\em The Computer Journal}, 55(6):653--666, 2012.
+
+\bibitem{bcgs12:ij}
+Jacques Bahi, Jean-Fran\c{c}ois Couchot, Christophe Guyeux, and Michel Salomon.
+\newblock Neural networks and chaos: Construction, evaluation of chaotic
+  networks, and prediction of chaos with multilayer feedforward network.
+\newblock {\em Chaos, An Interdisciplinary Journal of Nonlinear Science},
+  22(1):013122--1 -- 013122--9, March 2012.
+\newblock 9 pages.
+
+
+
+\bibitem{ccg15:ij}
+Jean-Fran\c{c}ois Couchot, Rapha\"el Couturier, and Christophe Guyeux.
+\newblock {STABYLO}: {STeganography with Adaptive, Bbs, and binarY embedding at
+  LOw cost}.
+\newblock {\em Annals of Telecommunications}, 2015.
+\newblock Available online. Paper version to appear.
+
+
+\bibitem{cds13:ij}
+Jean-Fran\c{c}ois Couchot, Karine Deschinkel, and Michel Salomon.
+\newblock Active {MEMS}-based flow control using artificial neural network.
+\newblock {\em Mechatronics}, 23(7):898--905, October 2013.
+\newblock Available online. Paper version to appear.
+
+\end{thebibliography}
+
+\subsection{Conférences internationales avec comité de sélection}
+
+\begin{thebibliography}{CHG{\etalchar{+}}14b}
+\makeatletter
+\addtocounter{\@listctr}{11}
+\makeatother
+
+\bibitem{aangc+15:ip}
+Bassam Alkindy, Huda Al'Nayyef, Christophe Guyeux, Jean-Fran\c{c}ois Couchot,
+  Michel Salomon, and Jacques Bahi.
+\newblock Improved core genes prediction for constructing well-supported
+  phylogenetic trees in large sets of plant species.
+\newblock In {\em IWBBIO 2015, 3rd Int. Work-Conf. on Bioinformatics and
+  Biomedical Engineering, Part I}, volume 9043 of {\em LNCS}, pages 379--390,
+  Granada, Spain, April 2015.
+
+\bibitem{acgm+14:ij}
+Bassam Alkindy, Jean-Fran\c{c}ois Couchot, Christophe Guyeux, Arnaud Mouly,
+  Michel Salomon, and Jacques Bahi.
+\newblock Finding the core-genes of chloroplasts.
+\newblock In {\em ICBBS 2014, 3rd Int. Conf. on Bioinformatics and Biomedical
+  Science}, number 4(5) in IJBBB, Journal of Bioscience, Biochemistery, and
+  Bioinformatics, pages 357--364, Copenhagen, Denmark, June 2014.
+
+\bibitem{akgcs+14:oip}
+Bassam Alkindy, Christophe Guyeux, Jean-Fran\c{c}ois Couchot, Michel Salomon,
+  and Jacques Bahi.
+\newblock Gene similarity-based approaches for determining core-genes of
+  chloroplasts.
+\newblock In {\em BIBM14, IEEE Int. Conf. on Bioinformatics and Biomedicine},
+  Belfast, United Kingdom, November 2014.
+\newblock Short paper.
+
+\bibitem{agcs+15:ip}
+Bassam Alkindy, Christophe Guyeux, Jean-Fran\c{c}ois Couchot, Michel Salomon,
+  Christian Parisod, and Jacques Bahi.
+\newblock Hybrid genetic algorithm and lasso test approach for inferring well
+  supported phylogenetic trees based on subsets of chloroplastic core genes.
+\newblock In {\em AlCoB 2015, 2nd Int. Conf. on Algorithms for Computational
+  Biology}, volume~* of {\em LNCS/LNBI}, pages ***--***, Mexico City, Mexico,
+  August 2015. Springer.
+\newblock To appear in the LNCS/LNBI series.
+
+\bibitem{aagp+15:ip}
+Reem Alsrraj, Bassam Alkindy, Christophe Guyeux, Laurent Philippe, and
+  Jean-Fran\c{c}ois Couchot.
+\newblock Well-supported phylogenies using largest subsets of core-genes by
+  discrete particle swarm optimization.
+\newblock In {\em CIBB 2015, 12th Int. Meeting on Computational Intelligence
+  Methods for Bioinformatics and Biostatistics}, pages ***--***, Naples, Italy,
+  September 2015.
+\newblock To appear.
+
+
+\bibitem{bcfg12a:ip}
+Jacques Bahi, Jean-Fran\c{c}ois Couchot, Nicolas Friot, and Christophe Guyeux.
+\newblock Application of steganography for anonymity through the internet.
+\newblock In {\em IHTIAP'2012, 1-st Workshop on Information Hiding Techniques
+  for Internet Anonymity and Privacy}, pages 96--101, Venice, Italy, June 2012.
+
+\bibitem{bcfg12b:ip}
+Jacques Bahi, Jean-Fran\c{c}ois Couchot, Nicolas Friot, and Christophe Guyeux.
+\newblock A robust data hiding process contributing to the development of a
+  semantic web.
+\newblock In {\em INTERNET'2012, 4-th Int. Conf. on Evolving Internet}, pages
+  71--76, Venice, Italy, June 2012.
+
+\bibitem{bcfg+13:ip}
+Jacques Bahi, Jean-Fran\c{c}ois Couchot, Nicolas Friot, Christophe Guyeux, and
+  Kamel Mazouzi.
+\newblock Quality studies of an invisible chaos-based watermarking scheme with
+  message extraction.
+\newblock In {\em IIHMSP'13, 9th Int. Conf. on Intelligent Information Hiding
+  and Multimedia Signal Processing}, pages 547--550, Beijing, China, October
+  2013.
+
+\bibitem{bcg11:ip}
+Jacques Bahi, Jean-Fran\c{c}ois Couchot, and Christophe Guyeux.
+\newblock Performance analysis of a keyed hash function based on discrete and
+  chaotic proven iterations.
+\newblock In {\em INTERNET 2011, the 3-rd Int. Conf. on Evolving Internet},
+  pages 52--57, Luxembourg, Luxembourg, June 2011.
+\newblock Best paper award.
+
+\bibitem{bcg11b:ip}
+Jacques Bahi, Jean-Fran\c{c}ois Couchot, and Christophe Guyeux.
+\newblock Steganography: a class of algorithms having secure properties.
+\newblock In {\em IIH-MSP-2011, 7-th Int. Conf. on Intelligent Information
+  Hiding and Multimedia Signal Processing}, pages 109--112, Dalian, China,
+  October 2011.
+
+
+\bibitem{bcgr11:ip}
+Jacques Bahi, Jean-Fran\c{c}ois Couchot, Christophe Guyeux, and Adrien Richard.
+\newblock On the link between strongly connected iteration graphs and chaotic
+  boolean discrete-time dynamical systems.
+\newblock In {\em FCT'11, 18th Int. Symp. on Fundamentals of Computation
+  Theory}, volume 6914 of {\em LNCS}, pages 126--137, Oslo, Norway, August
+  2011.
+
+\bibitem{bcgw11:ip}
+Jacques Bahi, Jean-Fran\c{c}ois Couchot, Christophe Guyeux, and Qianxue Wang.
+\newblock Class of trustworthy pseudo random number generators.
+\newblock In {\em INTERNET 2011, the 3-rd Int. Conf. on Evolving Internet},
+  pages 72--77, Luxembourg, Luxembourg, June 2011.
+
+\bibitem{BCDG07}
+Fabrice Bouquet, Jean-Fran\c{c}ois Couchot, Fr\'ed\'eric Dadeau, and Alain
+  Giorgetti.
+\newblock Instantiation of parameterized data structures for model-based
+  testing.
+\newblock In Jacques Julliand and Olga Kouchnarenko, editors, {\em B'2007, the
+  7th Int. B Conference}, volume 4355 of {\em LNCS}, pages 96--110, Besancon,
+  France, January 2007. Springer.
+
+\bibitem{CouchotD07IFM}
+Jean-Fran\c{c}ois Couchot and Fr\'ed\'eric Dadeau.
+\newblock Guiding the correction of parameterized specifications.
+\newblock In {\em IFM'07, 6th Int. Conf. on Integrated Formal Methods}, volume
+  4591 of {\em LNCS}, pages 176--194, Oxford, UK, July 2007. Springer.
+
+
+\bibitem{cds12:ip}
+Jean-Fran\c{c}ois Couchot, Karine Deschinkel, and Michel Salomon.
+\newblock Suitability of artificial neural network for {MEMS}-based flow
+  control.
+\newblock In Julien Bourgeois and Michel de~Labachelerie, editors, {\em dMEMS
+  2012, Workshop on design, control and software implementation for distributed
+  MEMS}, pages 1--6, Besan\c{c}on, France, April 2012. IEEE CPS.
+
+
+\bibitem{cgs09:ip}
+Jean-Fran\c{c}ois Couchot, Alain Giorgetti, and Nicolas Stouls.
+\newblock {G}raph {B}ased {R}eduction of {P}rogram {V}erification {C}onditions.
+\newblock In Hassen Sa\"{i}di and N.~Shankar, editors, {\em AFM'09, {A}utomated
+  {F}ormal {M}ethods (colocated with {CAV}'09)}, pages 40--47, Grenoble,
+  France, 2009. ACM Press.
+
+\bibitem{chgw+14:oip}
+Jean-Fran\c{c}ois Couchot, Pierre-Cyrille H\'eam, Christophe Guyeux, Qianxue
+  Wang, and Jacques Bahi.
+\newblock Pseudorandom number generators with balanced gray codes.
+\newblock In {\em Secrypt 2014, 11th Int. Conf. on Security and Cryptography},
+  pages 469--475, Vienna, Austria, August 2014.
+
+
+\bibitem{couchot07FTP}
+Jean-Fran\c{c}ois Couchot and T.~Hubert.
+\newblock A graph-based strategy for the selection of hypotheses.
+\newblock In {\em FTP'07, Int. Workshop on First-Order Theorem Proving},
+  Liverpool, UK, September 2007.
+
+\bibitem{couchot07cade}
+Jean-Fran\c{c}ois Couchot and S.~Lescuyer.
+\newblock Handling polymorphism in automated deduction.
+\newblock In {\em CADE'07, 21st Int. Conf. on Automated Deduction}, volume 4603
+  of {\em LNCS}, pages 263--278, Bremen, Germany, July 2007. Springer.
+
+
+\bibitem{fccg15:ip}
+Yousra~Ahmed Fadil, Jean-Fran\c{c}ois Couchot, Rapha\"el Couturier, and
+  Christophe Guyeux.
+\newblock Steganalyzer performances in operational contexts.
+\newblock In {\em IIH-MSP 2015, 11th Int. Conf. on Intelligent Information
+  Hiding and Multimedia Signal Processing}, pages ***--***, Adelaide,
+  Australia, September 2015.
+\newblock To appear.
+
+\end{thebibliography}
+
+\subsection{Communications orales invitées}
+
+J'ai été invité:
+\begin{itemize}
+
+\item au Workshop \og Théorie des réseaux booléens et ses applications en biologie\fg{}  
+à Nice en novembre 2014;
+
+\item à la journée \og Advances in Mobile Technologies Day\fg{}  par l'Université Antonine  (Liban) en mai 2013;
+
+\item au Séminaire MDSC (Modèles Discrets pour les Systèmes Complexes)
+  du laboratoire I3S sur le sujet \og Efficiently dealing with SMT-LIB provers in software verification\fg{} en décembre 2007.
+\end{itemize}
+
+\subsection{Communications diverses}
+\begin{thebibliography}{CHG{\etalchar{+}}14b}
+
+\makeatletter
+\addtocounter{\@listctr}{31}
+\makeatother
+
+\bibitem{acgs13:onp}
+Bassam Alkindy, Jean-Fran\c{c}ois Couchot, Christophe Guyeux, and Michel
+  Salomon.
+\newblock Finding the core-genes of chloroplast species.
+\newblock Journ\'ees SeqBio 2013, Montpellier, November 2013.
+
+
+
+
+\bibitem{BCVC10:ir}
+J.~M. Bahi, S.~Contassot-Vivier, and J.-F. Couchot.
+\newblock Convergence results of combining synchronism and asynchronism for
+  discrete-state discrete-time dynamic network.
+\newblock Research Report RR2010-02, LIFC - Laboratoire d’{I}nformatique de
+  l'{U}niversit\'{e} de {F}ranche {C}omt\'{e}, May 2010.
+
+
+\bibitem{Cou10:ir}
+J.-F. Couchot.
+\newblock Formal {C}onvergence {P}roof for {D}iscrete {D}ynamical {S}ystems.
+\newblock Research Report RR2010-03, LIFC - Laboratoire d’{I}nformatique de
+  l'{U}niversit\'{e} de {F}ranche {C}omt\'{e}, May 2010.
+
+\bibitem{chgw+14:onp}
+Jean-Fran\c{c}ois Couchot, Pierre-Cyrille H\'eam, Christophe Guyeux, Qianxue
+  Wang, and Jacques Bahi.
+\newblock Traversing a n-cube without balanced hamiltonian cycle to generate
+  pseudorandom numbers.
+\newblock 15-th Mons Theoretical Computer Science Days (15e Journ\'ees
+  Montoises d'Informatique Th\'eorique), Nancy, France, September 2014.
+
+
+\end{thebibliography}
+
+
+\begin{figure}[h]
+\begin{center}
+\begin{tabular}{|c|c|c|c|c|}
+\hline
+%& \multicolumn{2}{|c|}{Internationaux} &  {Nationaux} &  \\
+%\hline
+& Journaux & Conférences  & 
+Conférences  &  Divers\\
+& internationaux & internationales  & 
+nationales  &  \\
+
+\hline
+Pendant le doctorat &
+%journaux
+\cite{cdgr03:ij}
+&
+% conf inter
+\cite{cddg+04:ip,CGK05}
+
+&
+% conf nat
+\cite{cdgr04:onp,cg04:np}
+
+&
+% divers
+\cite{couchot04:onp}
+
+\\ \hline  
+En post-doctorat & 
+%journaux
+
+&
+% conf inter
+\cite{BCDG07,CouchotD07IFM,cgs09:ip,couchot07FTP,couchot07cade}
+
+&
+% conf nat
+
+
+&
+% divers
+
+
+\\ \hline  
+
+&
+%journaux
+&
+% conf inter
+\cite{aangc+15:ip,aagp+15:ip,acgm+14:ij,
+  akgcs+14:oip,agcs+15:ip}
+
+&
+% conf nat
+
+
+&
+% divers
+
+%%%%%%%%%%%%%%
+
+\\ %\cline{3-3}  
+
+Au DISC à FEMTO-ST&
+%journaux
+\cite{bcg12:ij,bcg11:ij,bcgs12:ij,ccg15:ij,cds13:ij}
+
+
+
+
+
+
+
+&
+% conf inter
+\cite{bcfg+13:ip,bcfg12a:ip,bcfg12b:ip,bcg11:ip,bcg11b:ip}
+
+&
+% conf nat
+
+
+&
+% divers
+\cite{acgs13:onp,BCVC10:ir,chgw+14:onp,Cou10:ir}
+
+
+
+\\ %\hline  
+
+&
+%journaux
+
+&
+% conf inter
+\cite{bcgr11:ip,bcgw11:ip,cds12:ip,chgw+14:oip,fccg15:ip}
+
+&
+% conf nat
+
+
+&
+% divers
+
+
+
+%%%%%%%%%%%%%
+
+
+\\ \hline  
+\end{tabular}
+\end{center}
+\caption{Bilan synthétique des publications}\label{fig:bilan}
+\end{figure}
+
+
+
+
+% \newpage
+% \section{Avis du directeur de l'Equipe}\label{sec:avis:directeur}

 
 

-\section{Avis du directeur de l'Equipe}\label{sec:avis:directeur}
+%\bibliographystyle{plain}
+%\0\bibliography{abbrev,biblioand}

 
 

-\bibliographystyle{alpha}
-\bibliography{biblio}
-\include{Bibliographie}

 
 
 \end{document}
 
 
 \end{document}