+\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.
+Le second concerne les systèmes dynamiques discrets
+et leurs applications (Sec.~\ref{sub:sdd}), 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étisé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
+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
+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{Les Systèmes dynamiques discrets (SDD)}\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. Cette section présente un ensemble
+de mes contributions dans cette thématique.
+
+
+\subsubsection{Convergence de systèmes dynamiques discrets}
+
+%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}
+
+
+\subsubsection{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.
+
+
+\subsubsection{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.
+La figure~\ref{fig:mems}, issue de~\cite{cds13:ij}, montre
+que notre approche a pu apprendre ce régime turbulent.
+Il est apparu comme intéressant 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}.
+
+\begin{figure}
+\begin{center}
+\includegraphics[scale=0.5]{test.pdf}
+\end{center}
+\caption{Prédiction d'une force issue d'un flux d'air
+ le long d'un véhicule avec injecteurs}\label{fig:mems}
+\end{figure}
+
+
+\subsubsection{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.
+
+
+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~\cite{cgh16:onp}
+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~\cite{bgco16:onp} dans un journal international.
+
+
+
+
+
+
+\subsubsection{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~\cite{bdcc15:onp}.
+
+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 et illustré à la figure~\ref{fig:STABYLO}.
+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é.
+
+
+
+\begin{figure}[h]
+ \begin{center}
+ \subfigure[Support]{
+ \includegraphics[scale=0.20]{lena512}
+ }
+ \subfigure[Message]{
+ \begin{minipage}[b]{0.28\linewidth}
+ \begin{flushleft}
+ \begin{scriptsize}
+ The skies they were ashen and sober;\linebreak
+ $\qquad$ The leaves they were crisped and sere—\linebreak
+ $\qquad$ The leaves they were withering and sere;\linebreak
+ It was night in the lonesome October\linebreak
+ $\qquad$ Of my most immemorial year;\linebreak
+ It was hard by the dim lake of Auber,\linebreak
+ $\qquad$ In the misty mid region of Weir—\linebreak
+ It was down by the dank tarn of Auber,\linebreak
+ $\qquad$ In the ghoul-haunted woodland of Weir.
+ \end{scriptsize}
+ \end{flushleft}
+ \end{minipage}
+ }
+ \subfigure[Contours]{
+ \includegraphics[scale=0.20]{edge7}
+ }
+ \subfigure[Image avec msg.]{
+ \includegraphics[scale=0.20]{lena7}
+ }
+
+ \end{center}
+ \caption{Embarquement d'un message dans une image selon STABYLO}\label{fig:STABYLO}
+\end{figure}
+
+
+
+\subsubsection{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 arbres phylogénétiques de qualité~\cite{agcs+15:ip,aangc+15:ip}.
+Une synthèse de ces arbres a été réalisée et est présentée à l'adresse~\url{http://meso.univ-fcomte.fr/peg/phylo}.
+
+
+Tous ces travaux ont été réalisés en collaboration avec M. Salomon et en co-encadrant
+le doctorat de B. Alkindy.
+
+
+
