[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\cite{cdgr03:ij,cddg+04:ip,cg04:np} 
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éfinies à l'aide de spécification ensemblises B~\cite{cdgr04:onp}.





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


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

Entre avril 2006 et aujourdh'ui, les recherches réalisées ont concerné plusieursdomaines 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:ih}) sur les systèmes 
dynamiques discrets et leurs applications, thématique 
sur laquelle j'ai été recruté pour travailler dans l'équipe AND du département
DISC. Enfin la section~\ref{sub:gen} présente comment j'ai réinvesti le nouveau 
domaine de la bio-info à l'aide de compétences connexes.
  

\subsection{Vérification de programmes par 
  preuve automatique}\label{sub:verif}

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{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  
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 par Pr. J. M.  Bahi en2005 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 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 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 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 en 2010
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.

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 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}\label{sub:gen}

Ayant acquis des compétences sur certaines structures de mathématiques 
discrètes (particulièrement théorie des graphe, 
relation d'équivalence,\ldots), j'ai pu contribuer en bio-informatique
en les réappliquant notamment.

Une de mes première piste de travail a été de proposer une méthode automatique 
de construction d'un ensemble de gènes communs (nommés core-génôm) 
à une famille de génômes.
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ènes est assimilé à son représentant de
classe dans chaque génôme. Le core-genome se déduit comme  l'intersection 
de tous les génôme. 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énômes de (trop)
petits cardinaux. J'ai contribué notamment 
à l'amélioration de la méthode en proposant une étape d'optimization issue 
d'une adaptation discrète la méthode d'essaims particulaires~\cite{aagp+15:ip}.




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

\subsection{Les codes de Gray}

L'utilisation des codes de Gray dans une démarche d'apprentissage 
(d'ecoulement 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 etre très petite tandis que le chemin (dans le 
cycle  hamitlonien) 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
dans l'étape de construction de fonctions chaotiques pour la génération 
de nombres pseudo aléatoire 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$, 
ce qui n'est pas raisonnable de mettre en  
pratique lorsque chacune d'entre-elle prend 1s. On peut peut-être
se contenter de code ``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'optenir des optimums locaux et trouver ainsi des codes presque approximés.


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

La démarche actuelle de génération de nombres pseudo-allé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. Le problème semble pouvoir se réécrire
comme un produit de deux automates à définir et à étudier. 
Je pense investiguer cette vois pour améliorer notre approche et 
s'affranchir, à terme, de tout autre générateur.
Les propriété établies notament 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 le autant efficace: le nombre de bits généré par surface
est plutôt faible. Nous allons exploiter les meilleurs démarches mises en 
exherbe lors de la rédaction d'un état de l'art exhaustif sur les PRNG 
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érér une fonction dont la matrice de Markov est doublement
stochastique, nous avons proposé principalement deux méthodes 
(génération puis test, suppresion de chemin hamiltonien dans un $n$-cube).  
Ces deux méthodes ne passent pas à l'échelle, même pour des $n$ de ptite taille.
Je pense attaquer ce problème algébriquement et en programmation logique avec 
contraintes. Dans le premier cas, on peut remarque composée de $1$ uniquement 
en $(i,i+1)$ est une réponse trivale au problème. Elle n'entre cependant dans 
aucune des solutions des deux premières démarches. 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 Loraine.
Le département DISC et l'équipe VESONTION 
a de fortes compétences en programmation logique avec 
contraintes. J'ai déjà démontré que ce problème peut être solluble 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érateur. 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.
Cependant, 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}
Jusqu'à présent, autant que je sache les méthodes algébriques 
de réducution de domaine (analyse par composant principaux, SVD) 
n'ont pas été intégrées dans les outils permettant de décider si un
média contient ou non un message caché. 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.

  

\subsection{Bio-informatique}

reconstruction d'ancètre






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