preuve promela:debut de traduction

[hdrcouchot.git] / demandeInscription / synthese.tex

\documentclass[a4paper,french,12pt]{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=1.5cm, vmargin=1.5cm }


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

%
%\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}
\renewcommand{\refname}{ }

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


\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é (devenu département DISC de FEMTO-ST), 
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^{ème}$ 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^{è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}


%\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.
Mon directeur de recherche pour cette HDR est Pr. J. {\sc Bahi} 
du département DISC. Son avis, ainsi que celui du directeur de l'équipe (Pr. R. {\sc Couturier}, du directeur de l'école doctorale (PR. P. {\sc Lutz}) 
et du directeur du département (Pr. O. {\sc Kouchnarenko}) sont donnés en annexes. 


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



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















%\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. 
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{sec:appl}
présente comment j'ai appliqué ces compétences théoriques et pratiques
en bio-informatique  et  dans les réseaux de capteurs.
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:oip,chgw+14:onp} s'appuie sur les codes 
de Gray, ou de manière équivalente sur les cycles hamiltoniens du graphe des
itérations.
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, Pr. C. Guyeux du DISC et Pr. S. Contassot
du LORIA est en cours de soumission~\cite{cgh16:onp}
dans un  journal international.

Enfin je co-encadre 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.
18 PRNGs de 4 familles (xorshift, LFSR, TGFSR, and LCG) ont été 
implantés sur  FPGA et ont pu être ainsi comparés pratiquement sur 
la même plate-forme. Une boite de post-processing implantant les itérations
chaotiques a été déployée et a permis d'améliorer les résultats statistiques.
Ceci a été valorisé par la publication~\cite{BCG16:ip}.




\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 Bitar--,
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é.
Ce travail a été accepté 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,accfg15:ip}.
Ceci se réalise en co-encadrant le doctorat de Y. Fadil. Nous avons de plus dans celui-ci
proposé d'exprimer les fonctions de distorsion comme des méthodes de calcul de gradient 
ou de matrice Hessienne. Ceci a donné lieu à la publication~\cite{ccfg16:ip}.  

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 C. Guyeux et 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é algorithmique.



\begin{figure}[h]
  \begin{center}
    \subfigure[Support]{
      \includegraphics[scale=0.17]{lena512}
    }
    \subfigure[Message]{
      \begin{minipage}[b]{0.33\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.17]{edge7}
    }
    \subfigure[Image avec msg.]{
      \includegraphics[scale=0.17]{lena7}
    }

  \end{center}
  \caption{Embarquement d'un message dans une image selon STABYLO}\label{fig:STABYLO}
\end{figure}

Enfin, les méthodes d'apprentissage ont largement progressé cette dernière décennie, 
particulièrement grâce aux implantations efficaces de deep-learning. Dans un travail en collaboration
avec Pr R. Couturier, Pr. C. Guyeux et Dr. M. Salomon, nous avons voulu étudier la 
faisabilité d'utiliser du deep-learning à base de convolutions comme outil de stéganalyse.
Ceci a donné lieu à l'encadrement d'un stagiaire en M2, D. Fache, et 
un rapport technique~\cite{CCGS16:ir}. Lorsque la clef d'embarquement est 
la même pour toutes les images, nous avons exhibé une architecture de réseau 
deep learning à base de convolutions qui améliore de manière significative tous les résultats connus en 
stéganalyse. La figure~\ref{fig:deep} montre que la détection est valide à 95\% 
(respectivement à 80\%) lorsque le taux d'embarquement est de 0,4 bit par pixel (resp. 0.1)
tandis que les meilleurs résultats connus sont de l'ordre de 85\% (resp. 70\%).
Cependant, ceci ne s'applique pas aux cas où les clefs sont distinctes.


\begin{figure}[h]
\centering
\subfigure[][WOW, $\alpha=0.4$~bpp]{%
\label{fig:accuracy_WOW_0.4}%
%\label{fig:ex3-a}%
\includegraphics[scale=0.39]{Training_wow_04.pdf}
}%
\hspace{4pt}%
\subfigure[][WOW, $\alpha=0.1$~bpp]{%
\label{fig:accuracy_WOW_0.1}%
\includegraphics[scale=0.39]{Training_wow_01.pdf}
}
\caption{Stéganalyse de WOW avec différents ratios d'embarquement}\label{fig:deep}
\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{Applications à d'autres sujets}\label{sec:appl}

\subsubsection{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)
petit cardinal. 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,aagc+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 Dr. M. Salomon et en co-encadrant 
le doctorat de B. Alkindy, soutenu en décembre 2015.

\subsubsection{Réseaux de capteurs}\label{sub:optim}

J'ai abordé avec Dr. A. Mostefaoui la thématique des réseaux de capteurs multimédia:
ce contexte scientifique 
a la particularité d'avoir des données volumineuses et qui requièrent un traitement
coûteux en énergie. L'enjeu consiste à optimiser la dépense énergétique en fonction de la qualité 
attendue. 
Dans le cadre d'un projet soutenu par la région de Franche-Comté, \og capteurs multimédias collaboratifs: une approche
intégrée de la sécurité et de la robustesse\fg{}, nous encadrons la doctorante 
N. Khernane sur ce sujet depuis novembre 2015.
Nous avons proposé un nouvel algorithme complètement distribué permettant d'optimiser 
la durée de vie d'un tel réseau de capteurs en fonction d'une qualité visuelle attendue.
Ce premier travail a été valorisé par une publication en conférence internationale~\cite{kcm16:ip}.



%\newpage
\section{Perspectives de recherche}
Les trois sections suivantes présentent quelques perspectives de recherche 
autour de la thématique des systèmes dynamiques discrets. 




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


Dans le cadre du doctorat de M. Bakiri, nous avons implanté sur  FPGA 
18 PRNGs de 4 familles (xorshift, LFSR, TGFSR, and LCG) ainsi que 
le post-processing implantant les itérations
chaotiques. Nous pensons étudier d'abord pratiquement l'intérêt de telles itérations
en termes de surface requise lors du déploiement et du nombre d'opérateurs nécessaires.
Les améliorations escomptées dans le paragraphe précédent seront réinvesties dans cette 
partie et celle-ci viendront nourrir le travail précédent. 




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{Les chemin Hamiltonien/ les codes de Gray}

Pour générer une fonction dont la matrice de Markov est doublement
stochastique
--condition nécessaire pour fournir une sortie uniformément distribuée--, nous avons proposé principalement la méthode de
suppression de chemin hamiltonien dans un $n$-cube. 

Un chemin hamiltonien pouvant être vu comme un code de Gray, nous sommes intéressés à la 
génération de ce genre de codes en privilégiant les codes de Gray équilibrés, 
c'est-à-dire ceux dont chaque bit est nié le même nombre de fois.
Cependant la méthode de Robinson et Cohn (permettant d'obtenir des codes de Gray globalement ``presque'' 
équilibrés) et leurs extensions sont indéterministes dans le sens où 
elles montrent l'existence d'une suite particulière sans donner sa construction.
Un premier verrou scientifique que je propose de lever consiste à proposer une solution 
algébrique (et donc un algorithme) donnant une solution à ce problème. 

Il est apparu récemment des algorithmes permettant d'obtenir des codes de Gray 
localement équilibrés, c.-à-d. où la longueur du plus grand nombre d'étapes entre 
deux changements d'un même bit est aussi petite que possible.
Dans tous les cas, aucun des ces codes n'est globalement équilibré ni même presque équilibré.
Cette double propriété serait cependant très intéressante aussi bien théoriquement que pratiquement
pour nos générateurs.
Un second verrou consistera à adapter ces algorithmes pour proposer des codes possédant les 
deux propriétés d'équilibrage.
Ce travail consistera d'abord à vérifier l'existence de codes pour des instances de petite 
taille, sans que cela soit trivial (par exemple pour $n=6$) et ce en travaillant en collaboration 
avec Pr S. Contassot, spécialiste en SDD et en calcul distribué.
 







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

De plus les résultats obtenus en stéganalyse à l'aide de deep learning à base de convolutions
sont très prometteurs  lorsque la clef qui a servi à l'embarquement est constante. 
Malheureusement, lorsque la clef varie, nous n'avons pas réussi à généraliser ces avancées.
Les démarches les plus efficaces demeurent 
celles obtenues par des approches classiques à base de caractéristiques statistiques (features) 
d'images.
Cependant, en étudiant plus finement les features, on constate que nombreuses sont celles qui sont aussi
basées sur des produits de convolution.
Je propose d'étudier exhaustivement ces features pour d'abord traduire
en deep-learning celles qui sont des convolutions directes. Il restera ensuite 
à adapter l'outil de deep learning aux caractéristiques restantes ce qui est un autre challenge 
scientifique. 



%\newpage
\section{Insertion dans l'équipe de recherche} 
Cette section donne quelques éléments factuels 
permettent d'apprécier mon insertion au sein  de cette équipe de recherche.



\subsection{Un défi de changement de thématique}
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.
Ce défi de changement de thématique a été attaqué dès mon recrutement.
En plus des 6 journaux dans cette nouvelle thématique, 
j'ai publié sur ces thématiques notamment dans
les conférences reconnues suivantes:
\begin{itemize}
\item  \cite{bcgr11:ip} de rang A et
\item \cite{BCG16:ip,ccfg16:ip,kcm16:ip, chgw+14:oip} de rang B.
\end{itemize}



\subsection{Appels à projet}


En 2014, j'ai participé 
au projet Jeune chercheur de l'UFC porté par
Christophe Guyeux dont le thème était 
\og la sécurisation numérique par chaos\fg{}.

J'ai répondu avec succès à l'appel à projets de la région de 
Franche-Comté en 2015: j'ai participé à l'élaboration du  
projet de \og capteurs multimédias collaboratifs: une approche
intégrée de la sécurité et de la robustesse\fg{} dont le porteur 
est M. A. Mostefaoui. Nous avons obtenu le financement d'une bourse doctorale 
pour la période d'oct. 2015--oct. 2018. Ce doctorat est co-encadré par 
M. A. Mostefaoui et moi-même.

J'ai répondu à de nombreux autres appels à projets sans succès: 
\begin{itemize}
\item porteur d'un projet ANR COSINUS 2009: \og 
A FRAMEwork for predicting the behavior of Dicrete Dynamic Systems\fg{}
avec l'I3S et le LORIA. 
\item participant à un projet ANR blanc en 2010: 
\og Unification des Systèmes Dynamiques Discrets \fg{}
avec l'I3S, le LORIA et le LIF de Marseille.
\item porteur d'un projet PEPS 2011 avec l'équipe MIE du département Energie de  FEMTO-ST.
\item participant à un projet PHC CAI YUANPEI 2014: \og Theoretical study, design, and circuit implementation of high dimensional integer domain chaotic systems \fg{} avec l'Université Technlogique de Guangdong.
\item porteur d'un projet PHC Cedre 2015: \og surveillance vidéo sécurisée et robuste par réseau de capteurs\fg{} avec l'Université Antonine.
\item participant à un  projet PHC Cedre 2015: \og 
méthodes et outils pour concevoir, évaluer et déployer des réseaux de capteurs 
pour l'agriculture au liban\fg{} avec l'Université Libanaise.
\item participant au projet PEPS JCJC INS2I 2015, sur 
\og Prédiction bio-informatique de l'évolution des génomes\fg{} avec le
LMB et le l'université de Neuchâtel en Suisse. 
\end{itemize}

\subsection{Collaborations}
J'ai établi des collaborations:
\begin{itemize}
\item avec A. Richard CR CNRS du laboratoire
I3S (Nice)- UMR CNRS 7271 sur la thématique des SDDs et leurs 
applications en Bio. Cela s'est traduit notamment avec 
la publication~\cite{bcgr11:ip}.

\item avec R. Darazy de l'Université Antonine au Liban. 
  J'ai co-encadré trois stages de Master 2 recherche avec
  des membres de cette université.
  J'ai un article de journal~\cite{bdcc15:onp} résumant un travail en collaboration
  avec R. Darazy.

\item avec Pr. S. Contassot-Vivier du LORIA (Nancy)- UMR CNRS 7503 
sur la thématique des SDDs, de leur convergence dans les itérations 
mixtes et de la générations de matrices de Markov doublement
stochastiques. Cela s'est traduit notamment avec 
le rapport~\cite{BCVC10:ir} et l'article de journal~\cite{cgh16:onp}, en cours de soumission
en journal international.

\item avec Pr. Y. Bailly et J.-C. Roy de l'équipe 
  MIE du département \'Energie de FEMTO-ST sur la thématique 
  de la prédiction d'écoulement d'un flux d'air le long d'un véhicule.
  Cela s'est traduit notamment avec 
  les publications~\cite{cds13:ij,cds12:ip}.

\item avec Dr. Qianxue Wang de l'Université Technlogique de Guangdong 
sur la génération de nombres pseudo aléatoires. 
Nous avons collaboré sur deux publications~\cite{bcgw11:ip,chgw+14:oip}.

\end{itemize}


\subsection{Invitations}
J'ai été invité:
\begin{itemize}
\item à la soutenance de Thèse de M. J.-L. Joly sur {\em 
Contributions à la génération aléatoire pour des classes d'automates finis} en tant qu'invité
le 23 mars 2016 à l'Université de Franche-Comté;
\item au workshop \og Théorie des réseaux booléens et ses applications en
  biologie\fg{}  à Nice en novembre 2014 (20 participants);
\item à la journée \og Advances in Mobile Technologies Day\ fg{} 
  organisée par l'Université Antonine au Liban en mai 2013 (10 participants);
\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 (30 participants).
\end{itemize}

\subsection{Organisation d'événements scientifiques}

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
dont l'url est
\url{http://www.iaria.org/conferences2012/IHTIAP.html}.
Le comité de programme était composé de 18 chercheurs internationaux 
(dont je faisais aussi partie). 
Il s'est  déroulé sur 1/2 journée et 5 chercheurs ont présenté leurs travaux.
Le taux d'acceptation des articles a été de 41\%. 


J'ai été responsable de la publication des actes dans les conferences 
{\em 19th IEEE International Conference on Computational Science and Engineering (CSE 2016)},
{\em 15th International Symposium on Distributed Computing and Applications to Business, Engineering and Science (DCABES 2016)}
et
{\em 14th IEEE/IFIP International Conference on Embedded and Ubiquitous Computing (EUC 2016)}.



J'ai fait partie des comités de programme des conférences \og int. conf. on Evolving Internet \fg{}, (2013, 2014) 
et IHTIAP 2012.

J'ai rédigé des rapports de relecture pour les journaux internationaux 
suivants: 
\begin{itemize}
\item Springer Annals of Telecommunications 2013 (2);
\item The computer Journal 2014 (1); 
\item Springer Multimedia Tools and Applications 2014 (1);
\item International Journal of Bioinformatics Research 2015 (1);
\item International Journal of Computer Science and Application 2015 (1);
\item MDPI Symmetry 2016 (3);
\item Hindawi Journal of Electrical and Computer Engineering 2016 (1).
\end{itemize}
et pour les conférences suivantes:
\begin{itemize}
\item MAJECSTIC (2005 (2), 2007 (2));
\item B 2007 (1), A-BZ 2008 (1);
\item Evolving Internet \fg{}, (2012 (2), 2013 (2), 2014 (1));
\item 2015 IEEE/SICE International Symposium on System Integration (1);
\item 2016 IEEE International Conference on Computational Science and Engineering (CSE 2016)  (4);

\end{itemize}

Membre du GDR codes et cryptographie, j'ai 
participé aux Journées Codes et Stéganographie en 2012 (Rennes) 
où j'ai présenté \og Steganography: secure and robust algorithms \fg{} et en 2013 (Paris).





%\newpage
\section{Encadrement et co-encadrement d'étudiants} 

\subsection{Thèse d'université}
J'ai co-encadré:
\begin{itemize}
\item
(à 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 a été soutenu le 17 décembre 2015.
Ce travail de thèse a donné lieu à 6 publications dans des conférences 
internationales~\cite{aangc+15:ip,acgm+14:ij,akgcs+14:oip,agcs+15:ip,aagp+15:ip, aagc+15:ip} et une communication nationale~\cite{acgs13:onp}.
\end{itemize}

Je co-encadre:
\begin{itemize}
\item  (à hauteur de 50\%) avec Pr. C. 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 à 3 publications dans des conférences
internationales~\cite{fccg15:ip,accfg15:ip,accfg15:ip}.
                
\item  (à hauteur de 50\%) avec Pr. C. 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 
août 2017.     
Ce travail de thèse a donné lieu à 1 publication dans un journal international 
en cours de soumission~\cite{bgco16:onp} et une conférence internationale~\cite{bgco16:onp}.

\item  (à hauteur de 50\%) avec  Dr. A. Mostefaoui (50\%)
le doctorat de  Nesrine Khernane
sur
une approche
intégrée de la sécurité et de la robustesse dans les capteurs multimédias collaboratifs. 
Le doctorat a commencé en novembre 2015 et devrait être soutenu en 
novembre 2018.  
Ce travail de thèse a donné lieu à 1 publication dans une conférence internationale~\cite{fccg15:ip}.
\end{itemize}


\subsection{Master 2 recherche}

J'encadre:

\begin{itemize}
\item le stage de recherche de Master 2 de D. Fache
sur une étude théorique et pratique du Deep Learning, application à la stéganalyse.
Le stage a commencé en mars 2016 et devrait être soutenu en septembre 2016. 
\end{itemize}

J'ai co-encadré:
\begin{itemize}
\item  (à hauteur de 34\%) avec Raphael Couturier (33\%) et 
Rony Darazi -- Université Antonine au Liban--(33\%)
le stage de recherche de Master 2 de  Ahmad Bitar
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~\cite{bdcc15:onp}.
\item  (à 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. 


\item (à 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 a été soutenu le 31 août 2015. 
\end{itemize}



%\newpage
\section{Participation à des tâches d'intérêt collectif}

\subsection{Tâches d'enseignement} 
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{}. Ce sont des
  promotions d'une vingtaine d'étudiants à chaque fois;
\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{}. Ce sont des
  promotions d'une vingtaine d'étudiants à chaque fois;
\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}

\subsection{Responsabilités} 

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. 
J'ai participé à ce titre à l'élaboration des parties de mathématiques du 
PPN du DUT d'informatique, à Dijon en 2011 et Orléans en 2012.  
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. 

\subsection{Montage de projets BQF}
J'ai monté avec succès deux projets BQF au sein de l'UFC autour
de la programmation mobile en 2009 et 2014. 
Ces projets BQF ont permis l'achat de smartphones et ordinateurs 
portables pour les projets d'étudiants du département d'informatique de l'IUTBM. 


\subsection{\`A l'extérieur de l'université}

Je suis régulièrement membre de jury des épreuves TIPE, épreuves communes
à 90 concours d'ingénieurs (sessions 2012, 2015 et 2016) et fournis  
à chaque session des sujets scientifiques pour l'épreuve.




%\newpage
\section{Publications après la thèse}\label{sec:publi}
Le tableau de la figure~\ref{fig:bilan} donné 
ci dessous synthétise les références détaillées ci-après.


\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{BCG16:ip,aangc+15:ip,acgm+14:ij,
  akgcs+14:oip,agcs+15:ip,aagp+15:ip}

&
% conf nat


&
% divers

%%%%%%%%%%%%%%

\\ %\cline{3-3}  

Au DISC à FEMTO-ST&
%journaux
\cite{bcg12:ij,bcg11:ij,bcgs12:ij,cds13:ij,ccg15:ij,bdcc15:onp}







&
% conf inter
\cite{aagc+15:ip,bcfg12a:ip,bcfg12b:ip,bcfg+13: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,accfg15:ip}

&
% conf nat


&
% divers

\\ %\hline  

&
%journaux

&
% conf inter
\cite{ccfg16:ip,kcm16:ip}

&
% conf nat


&
% divers


%%%%%%%%%%%%%


\\ \hline  
\end{tabular}
\end{center}
\caption{Bilan synthétique des publications}\label{fig:bilan}
\end{figure}



\subsection{Journaux internationaux avec comité de sélection}

\vspace{-2em}
\begin{thebibliography}{CHG{\etalchar{+}}14b}

\makeatletter
\addtocounter{\@listctr}{6}
\makeatother




\bibitem{bdcc15:onp}
Ahmad Bitar, Rony Darazi, Jean-François Couchot, and Raphaël Couturier.
\newblock Blind digital watermarking in pdf documents using spread transform
  dither modulation.
\newblock{\em Multimedia Tools and Applications}, 
1573-7721:1--19, November 2015.

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


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









\end{thebibliography}




\subsection{Journaux internationaux avec comité de sélection (en cours de soumission)}

\vspace{-2em}
\begin{thebibliography}{CHG{\etalchar{+}}14b}

\makeatletter
\addtocounter{\@listctr}{12}
\makeatother



\bibitem{cgh16:onp}
Jean-François Couchot, Sylvain Contassot-Vivier, Christophe Guyeux, and Pierre-Cyrille H\'eam.
\newblock Random walk in a n-cube without hamiltonian cycle to chaotic
  pseudorandom number generation: Theoretical and practical considerations.
\newblock  in submission to Elsevier Chaos, Solitons \& Fractal, August 2016.

\bibitem{bgco16:onp}
Mohammed Bakiri, Christophe Guyeux, Jean-Fran\c{c}cois Couchot, and
  Abdelkrim~Kamel Oudjida.
\newblock Survey on hardware implementation of random number generators on
  fpga: Theory and experimental analyses.
\newblock in submission to the ACM Computing Surveys journal, August 2015.








\end{thebibliography}

\subsection{Conférences internationales avec comité de sélection}
\vspace{-2em}
\begin{thebibliography}{CHG{\etalchar{+}}14b}
\makeatletter
\addtocounter{\@listctr}{14}
\makeatother


\bibitem{BCG16:ip}
Bakiri Mohammed, Jean-François Couchot, and Christophe Guyeux.
\newblock  FPGA Implementation of F2-Linear Pseudorandom Number Generators based on Zynq MPSoC: A Chaotic Iterations Post Processing Case Study
\newblock In {\em Secrypt 2016, 13th Int. Conf. on Security and Cryptography},  pages ***--***,
  Lisboa, Portugal, July 2016.

\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~9199 of {\em LNCS}, pages 83--96, Mexico City, Mexico,
  August 2015. Springer.


\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{aagc+15:ip}
B. AlKindy, B. Al{-}Nuaimi, C. Guyeux, J.-F. Couchot, M. Salomon, R. Alsrraj, and Laurent Philippe,
\newblock Binary Particle Swarm Optimization Versus Hybrid Genetic Algorithm
               for Inferring Well Supported Phylogenetic Trees.
\newblock{\em Computational Intelligence Methods for Bioinformatics and Biostatistics
               - 12th International Meeting, {CIBB} 2015,
             Revised Selected Papers}, pages 165--179, September 2015.



\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{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{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{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 429--432, Adelaide,
  Australia, September 2015.

\bibitem{accfg15:ip}
B. Al Bouna and J. F. Couchot and R. Couturier and Y. A. Fadil and C. Guyeux.
\newblock Performance Study of Steganalysis Techniques.
\newblock In {\em Applied Research in Computer Science and Engineering (ICAR), 2015 International Conference on}, pages 1--7, Lebanon, October 2015.


\bibitem{ccfg16:ip}
Jean-François Couchot, Raphaël Couturier, Yousra Ahmed Fadil and Christophe Guyeux.
\newblock A Second Order Derivatives based Approach for Steganography.
\newblock In {\em Secrypt 2016, 13th Int. Conf. on Security and Cryptography},  pages ***--***,
  Lisboa, Portugal, July 2016.

\bibitem{kcm16:ip}
N. Khernane, J.-F. Couchot, A. Mostefaoui.
\newblock Maximizing Network Lifetime in Wireless Video Sensor Networks Under Quality Constraints.
\newblock In {\em MOBIWAC 2016: The 14th ACM* International Symposium on Mobility Management and Wireless Access} Malta,  to appear, November, 2016.

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

\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}
\vspace{-2em}
\begin{thebibliography}{CHG{\etalchar{+}}14b}

\makeatletter
\addtocounter{\@listctr}{39}
\makeatother

\bibitem{CCGS16:ir}
J.-F. Couchot,  R. Couturier, C. Guyeux, and M. Salomon
\newblock Steganalysis via a Convolutional Neural Network using Large Convolution Filters for Embedding Process with Same Stego Key.
\newblock July, 2016.

\bibitem{acgs13:onp}
 Bassam Alkindy, Jean-François Couchot, Christophe Guyeux, and Michel Salomon. 
\newblock Finding the core-genes of Chloroplast Species. 
\newblock  Journées SeqBio 2013, Montpellier, November 2013. 


\newblock Finding the core-genes of chloroplast species.

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






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

%\bibliographystyle{plain}
%\bibliography{abbrev,biblioand}



\end{document}