1 \documentclass[a4paper,french,12pt]{article}
2 %\usepackage{hyperlatex}
3 \usepackage[utf8]{inputenc}
4 \usepackage[T1]{fontenc}
10 \usepackage[amsmath,thmmarks,thref,framed]{ntheorem}
11 \usepackage[dvips]{graphics}
13 \usepackage{epsfig,psfrag}
14 \usepackage{subfigure}
18 \usepackage{longtable}
21 %\usepackage{slashbox}
25 \usepackage[frenchb]{babel}
26 \usepackage[a4paper]{geometry}
30 \geometry{hmargin=1cm, vmargin=1.5cm }
33 \newcommand{\JFC}[1]{\begin{color}{green}\textit{#1}\end{color}}
34 \newcommand{\etalchar}[1]{$^{#1}$}
37 %\lstset{% general command to set parameter(s)
38 %basicstyle=\small, % print whole listing small
39 %keywordstyle=\color{black}\bfseries\underbar,
40 % underlined bold black keywords
41 %identifierstyle=, % nothing happens
42 %commentstyle=\color{white}, % white comments
43 %stringstyle=\ttfamily, % typewriter type for strings
44 %extendedchars = true,
45 %showstringspaces=false} % no special string spaces
51 %backref=true, %permet d'ajouter des liens dans...
52 %pagebackref=true,%...les bibliographies
53 %hyperindex=true, %ajoute des liens dans les index.
54 colorlinks=true, %colorise les liens
55 breaklinks=true, %permet le retour à la ligne dans les liens trop longs
56 urlcolor= blue, %couleur des hyperliens
57 linkcolor= blue, %couleur des liens internes
58 %bookmarks=true, %créé des signets pour Acrobat
59 bookmarksopen=true, %si les signets Acrobat sont créés,
60 %les afficher complÚtement.
61 pdftitle={Demande d'inscription à l'HDR de JF COUCHOT}, %informations apparaissant dans
62 pdfauthor={Jean-Fran\c{c}ois Couchot}, %dans les informations du document
63 pdfsubject={Demande d'inscription à l'HDR de JF COUCHOT} %sous Acrobat.
71 \newcommand{\inputladot}[2]{
73 \includegraphics[width=#2]{#1.dot.ps}
76 \setcounter{secnumdepth}{4}
78 \renewcommand{\thesection}{\Roman{section}}
79 %\renewcommand{\thesubsection}{~~~~\arabic{subsection}}
80 %\renewcommand{\theparagraph}{~~~~~~~~\arabic{paragraph}}
83 \renewcommand{\refname}{ }
85 \title{Mémoire de synthèse des activités de recherche et d'encadrement}
86 \author{Jean-Fran\c{c}ois {\sc Couchot}}
92 \section{Curriculum vit{\ae}}
97 \item \textbf{web:} \url{http://members.femto-st.fr/jf-couchot/}
98 \item \textbf{courrier:}
99 %\begin{minipage}[t]{10cm}
100 FEMTO-ST, dpt DISC, IUT BM, 19 rue du maréchal Juin, 90000 Belfort
102 \item \textbf{mail:} \url{couchot@femto-st.fr}
103 \item\textbf {tel:} (+33) (0)3 84 58 77 38
104 \item\textbf {gsm:} (+33) (0)6 76 06 68 94
107 \subsection{Diplômes universitaires}
109 \item{\bf{91:}} Baccalauréat série C mention AB, Besançon.
110 \item{\bf{95:}} Maîtrise de mathématiques pures, Université de
113 CAPES de mathématiques, IUFM d'Auvergne.
115 Maîtrise d'informatique, mention B (UFC).
117 DEA Informatique, option {\em Génie Logiciel} (UFC). Stage intitulé {\em Atteignabilité d'états et spécifications
118 logico-ensemblistes}. Major de promotion, mention TB.
119 \item{\bf{avril 06:}}
120 Doctorat en informatique au Laboratoire d'Informatique
121 de l'Université de Franche Comté (devenu département DISC de FEMTO-ST),
122 sur la {\em vérification d'invariants par superposition},
123 mention très honorable.
127 \subsection{Fonctions et expériences professionnelles}
129 \item{\bf{95-00:}} Enseignant en mathématiques dans le secondaire,
130 successivement à Aurillac(15), Beaune(21), Belfort(90) et
132 \item{\bf{sept. 00-06:}} PrCe $71^{ème}$ section, Unité de Formation
133 et de Recherche (UFR) Sciences du
134 Langage de l'Homme et de la Société (SLHS) à l'UFC.
135 \item{\bf{sept. 06-07:}} Post-doctorant INRIA (projet ProVal) sur le
136 thème de l'intégration de preuves interactives dans des preuves
137 automatiques (et vice-versa). %pour la vérification de programmes C embarqués.
138 \item{\bf{sept. 07-08:}} PrCe $71^{ème}$ section, UFR SLHS à l'UFC.
139 \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).
140 \item{\bf{nov. 10- nov. 14:}} \'Elu au Conseil d'Institut de l'IUT BM.
145 \section{Nom et type de l'équipe de recherche}
147 Je suis membre de l'équipe Algorithmique Numérique Distribuée (AND) du
148 Département d'Informatique des Systèmes Complexes (DISC)
149 du laboratoire FEMTO-ST.
150 Je relève de l'école doctorale 37 Sciences Pour l'Ingénieur et Microtechniques (SPIM) de l'UFC.
154 \subsection{Avis du directeur de l'équipe}\label{sec:avis:directeur:equipe}
156 \subsection{Avis du directeur de recherche}\label{sec:avis:directeur:recherhce}
158 \subsection{Avis du directeur de l'école doctorale}\label{sec:avis:directeur:spim}
162 \section{Résumé de la thématique de la thèse d'université}
163 On considère en entrée de la démarche une description
164 mathématique d'un programme: par exemple une fonction enrichie avec
165 une spécification du contexte dans lequel elle est invoquée (la pré-condition) et
166 une spécification exprimant quelles propriétés sont garanties en retour (la
167 post-condition). Lorsque pré-condition et post-condition sont équivalentes,
168 on parle d'invariant.
169 La thématique de \emph{vérification de programmes par preuve automatique}
170 consiste à tout d'abord construire des formules mathématiques
171 qui doivent être vraies si et seulement si
172 la post-condition est établie par le programme sous hypothèse de pré-condition,
174 décharger ces formules dans des prouveurs de théorèmes.
175 Cette thématique est au c{\oe}ur des travaux de recherche effectués
176 pendant mon doctorat et le post-doctorat qui a suivi à l'INRIA.
180 Durant mon travail de thèse intitulée
181 {\em vérification d'invariants par superposition},
182 j'ai proposé différentes traductions en logique équationnelle~\cite{cdgr03:ij,cddg+04:ip,cg04:np,couchot04:onp}
183 des obligations de preuve,
184 dans l'objectif de faire converger
185 le plus rapidement possible un prouveur par superposition qui les décharge.
186 J'ai démontré la correction et la complétude partielle de la démarche et
187 ai montré que la démarche supplante celles basées sur la
188 logique WS1S et l'outil MONA.
189 J'ai appliqué ceci à la vérification de protocoles notamment d'exclusion
190 mutuelle~\cite{CGK05} définis à l'aide de spécifications ensemblistes B~\cite{cdgr04:onp}.
196 \subsection*{Publications issues de ces recherches}
199 \begin{thebibliography}{9}
201 Jean-Fran\c{c}ois Couchot, Alain Giorgetti, and Nikolai Kosmatov.
202 \newblock A uniform deductive approach for parameterized protocol safety.
203 \newblock In David~F. Redmiles, Thomas Ellman, and Andrea Zisman, editors, {\em
204 ASE}, pages 364--367. ACM, 2005.
208 Jean-Fran\c{c}ois Couchot, Fr\'ed\'eric Dadeau, D.~D\'eharbe, Alain Giorgetti,
210 \newblock Proving and debugging set-based specifications.
211 \newblock In A.~Cavalcanti and P.~Machado, editors, {\em WMF'03 proceedings},
212 volume~95 of {\em ENTCS, Electronic Notes in Theoretical Computer Science},
213 pages 189--208, Campina Grande, Brazil, May 2004.
216 Jean-Fran\c{c}ois Couchot, D.~D\'eharbe, Alain Giorgetti, and S.~Ranise.
217 \newblock Scalable automated proving and debugging of set-based specifications.
218 \newblock {\em Journal of the Brazilian Computer Society (JBCS)}, 9(2):17--36,
220 \newblock ISSN 0104-6500.
223 Jean-Fran\c{c}ois Couchot and Alain Giorgetti.
224 \newblock Analyse d'atteignabilit\'e d\'eductive.
225 \newblock In Jacques Julliand, editor, {\em Congr\`es Approches Formelles dans
226 l'Assistance au D\'eveloppement de Logiciels, AFADL'04}, pages 269--283,
227 Besan\c{c}on, France, June 2004.
230 Jean-Fran\c{c}ois Couchot, D.~D\'eharbe, Alain Giorgetti, and S.~Ranise.
231 \newblock {B}arvey: {V}\'erification automatique de consistance de machines
233 \newblock In Jacques Julliand, editor, {\em AFADL'04, Approches Formelles dans
234 l'Assistance au D\'eveloppement de Logiciels,} pages 369--372, Besan\c{c}on,
236 \newblock Session outils.
239 \bibitem{couchot04:onp}
240 Jean-Fran\c{c}ois Couchot.
241 \newblock V\'erification d'invariant par superposition.
242 \newblock In {\em {MAJECSTIC}'04, {MA}nifestation de {JE}unes {C}hercheurs
243 {STIC}}, Calais, France, October 2004.
244 \newblock Actes en ligne sur { t
245 http://lil.univ-littoral.fr/\~{}lewandowski/majecstic/programme.html}.
248 \end{thebibliography}
265 \section{Exposé des recherches réalisées au cours de la période postdoctorale}
267 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})
268 est une suite directe des travaux de thèse.
269 Le second concerne les systèmes dynamiques discrets
270 et leurs applications (Sec.~\ref{sub:sdd}), thématique
271 pour laquelle j'ai été recruté dans l'équipe AND du département
272 DISC. Enfin la section~\ref{sub:gen} présente comment je me suis investi dans
273 le domaine de la bio-informatique à l'aide de compétences connexes.
274 Ces travaux ont été valorisés par des publications dont les références sont données à la section~\ref{sec:publi} et synthéthisées à la figure~\ref{fig:bilan}
277 \subsection{Vérification de programmes par
278 preuve automatique}\label{sub:verif}
280 Lors de mon post-doctorat à l'INRIA, j'ai d'abord montré qu'il était possible
281 d'instancier des contre-exemples~\cite{BCDG07} et de voir
282 si ceux-ci sont atteignables~\cite{CouchotD07IFM} lorsque
283 l'obligation de preuve à vérifier n'est pas établie.
284 Ceci peut aider l'ingénieur à corriger ses modèles.
285 Je me suis ensuite intéressé à la
286 logique du premier ordre polymorphe.
287 Dans ce but, j'ai présenté un réducteur de logique
288 polymorphe vers de la logique sans sorte et de la logique multi-sortes
289 du premier ordre, préservant la correction et la
290 complétude~\cite{couchot07cade}.
291 Toujours pendant mon post-doctorat, face au problème d'explosion
292 combinatoire rencontré
293 lors de déduction automatique, j'ai présenté une approche
295 formules~\cite{couchot07FTP, cgs09:ip} de type SMT-LIB
296 basée sur la sélection des hypothèses les plus
298 L'approche a été implantée et validée sur un exemple industriel réel
299 de 5000 lignes de Code C annoté fourni par Dassault aviation.
306 \subsection{Les Systèmes dynamiques discrets (SDD)}\label{sub:sdd}
307 Un système dynamique discret (SDD) est une fonction $f$
308 du $n$-cube ($\{0,1\}^n$) dans lui même et un mode opératoire
309 (parallèle, unaire, généralisé) qui peut être itéré
310 en synchrone ou en asynchrone. Cette section présente un ensemble
311 de mes contributions dans cette thématique.
314 \subsubsection{Convergence de systèmes dynamiques discrets}
316 %Ils ont été étudiés à de maintes reprises ~\cite{Rob95,Bah00,bcv02}.
317 Pour chacun de ces modes, il existe des critères (suffisants) de convergence
318 globale ou locale, souvent basés sur le fait que $f$
319 est un opérateur contractant dans un espace.
321 Les modes asynchrones ont une dynamique avec plus de liberté
322 puisqu'ils autorisent chaque élément à modifier sa valeur avant
323 de connaître les valeurs des autres éléments dont il dépend.
324 Cependant, lorsque les calculs à effectuer sur certains n{\oe}uds
325 sont coûteux en temps et/ou que les temps de communication sont élevés,
326 ces modes peuvent présenter une convergence plus rapide que le cas synchrone.
328 J'ai formalisé le mode des
329 \emph{itérations mixtes} (introduit par Pr. J. M. Bahi en 2005 notamment)
330 qui combine synchronisme et asynchronisme.
331 Intuitivement, les n{\oe}uds qui pourraient engendrer des cycles dans
332 les itérations asynchrones sont regroupés dans une même classe.
333 Les noeuds à l'intérieur de celle-ci seront itérés de manière
334 synchrone et les itérations asynchrones sont conservées entre les groupes.
335 Pour gommer les différences entre les n{\oe}uds d'une même classe
336 lorsqu'ils sont vus depuis des n{\oe}uds extérieurs, j'ai défini le
337 mode des \emph{itérations mixtes avec délais uniformes}.
338 J'ai pu ainsi énoncer puis démontrer un théorème
339 établissant que pour des conditions classiques de convergence des itérations
340 synchrones d'une fonction $f$, les itérations mixtes à délai uniforme
341 convergent aussi vers le même point fixe.
342 Ceci a été synthétisé dans~\cite{BCVC10:ir}.
345 L'étude de convergence de SDDs de modèles de petite taille
346 est simple à vérifier pratiquement pour le mode synchrone parallèle:
347 l'espace d'intérêt est fini.
348 C'est beaucoup plus complexe lorsqu'on traite des itérations
349 unaires, voire généralisées
350 asynchrones et mixtes prenant de plus en compte les délais.
351 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.
352 Cependant, comme ces implantations ne sont pas exhaustives, elles ne sont intéressantes que lorsqu'elles fournissent un contre-exemple.
353 Lorsqu'elles exhibent une convergence,
354 cela ne permet que de donner une intuition de convergence, pas une preuve.
355 Autant que je sache, aucune démarche de preuve formelle automatique
356 de convergence n'avait jamais été établie.
359 J'ai démontré qu'on peut simuler
360 des SDDs selon tous les modes pour établir
361 formellement leur convergence (ou pas).
362 Cette simulation est basée sur l'outil SPIN de \emph{Model-Checking}.
363 Pour traiter le problème d'explosion
364 combinatoire, les outils de cette classe
365 appliquent des méthodes d'ordre partiel, d'abstraction,
366 de quotientage selon une relation d'équivalence.
367 J'ai présenté pour cela une démarche de traduction d'un SDD
369 J'ai énoncé puis prouvé ensuite la correction et la complétude de la démarche.
370 Des données pratiques comme la complexité et des synthèses d'expérimentation
371 ont aussi été fournies.
372 Ceci a été synthétisé dans~\cite{Cou10:ir}
375 \subsubsection{Construction de fonctions chaotiques}
376 Je me suis intéressé ensuite à l'étude du problème dual
377 de l'étude de divergence d'un SDD.
378 Le Pr. C. Guyeux de l'équipe AND a proposé dans sa thèse en 2010
379 une caractérisation des fonctions $f$ de $\{0,1\}^n$ dans lui-même
380 dont les itérations sont chaotiques selon Devanney pour un mode donné:
381 il est nécessaire et suffisant que son graphe des itérations soit
383 J'ai proposé plusieurs méthodes de construction de
384 fonctions ayant de tels graphes d'itérations~\cite{bcgr11:ip,chgw+14:onp}.
386 Dans la première~\cite{bcgr11:ip},
387 l'algorithme enlève des arcs et vérifie ensuite que
388 la forte connexité est maintenue.
389 Même si cet algorithme retourne toujours des fonctions dont le graphe
390 des itérations est fortement connexe, il n'en est pas pour autant efficace
391 car il nécessite une vérification à posteriori de la
392 forte connexité sur le graphe entier composé de $2^n$ sommets.
393 La seconde méthode propose une solution à ce problème en présentant
394 des conditions suffisantes sur un graphe à $n$ sommets
395 qui permettent d'obtenir des graphes d'itérations fortement connexes.
396 Ce théorème a aussi été prouvé dans~\cite{bcgr11:ip}
397 et des instanciations effectives
399 Une troisième méthode~\cite{chgw+14:onp} s'appuie sur les codes
400 de Gray, ou de manière équivalente sur les cycles hamiltoniens du graphe des
402 % : un cycle qui visite chaque n{\oe}ud exactement une fois est un
403 % \emph{cycle hamiltonien}.
404 %La démarche consiste à enlever du graphe un de ses cycles hamiltoniens dont
405 %la démarche de génération est un problème connu.
407 Ces méthodes ont permis d'étendre à l'infini la classe des fonctions
408 dont les itérations sont chaotiques.
411 \subsubsection{Apprentissage par réseaux neuronaux}
412 Nous disposons grâce aux travaux présentés à la section précédente d'un grand
413 nombre de fonctions dont les itérations sont chaotiques.
414 Nous avons entrepris d'étudier ces itérations et plus particulièrement leur
415 apprentissage par un réseau de neurones.
416 J'ai notamment pu contribuer à montrer pratiquement qu'il
417 est très difficile (voir impossible) de les prédire
418 à l'aide d'outils d'intelligence artificielle~\cite{bcgs12:ij}.
421 Nous nous sommes attaqués parallèlement
422 à un problème physique d'optimisation de
423 l'écoulement d'un flux d'air le long d'un véhicule.
424 Ce flux peut être modifié si l'on active des injecteurs d'air placés
425 par exemple sur le becquet du véhicule.
426 Le flux d'air peut être modélisé à l'aide d'équations de Navier-Stokes
427 dont on ne connaît pas de méthode analytique de résolution.
428 De plus, le nombre de Reynolds calculé dans cette situation fait apparaître
429 que le régime est extrêmement turbulent, donc difficile à prévoir.
431 continuer nos expériences d'apprentissage à l'aide
432 de réseau de neurones dans ce contexte.
433 La figure~\ref{fig:mems}, issue de~\cite{cds13:ij}, montre
434 que notre approche a pu apprendre ce régime turbulent.
435 Il est apparu comme intéressant de mémoriser les configurations
436 représentant l'état des actionneurs à l'aide de nombres binaires.
437 De plus les codes de Gray (dont deux mots adjacents ne diffèrent que d'un
438 bit) se sont présentés comme une des manières de mémoriser les sorties du
439 réseau de neurones comme un seul nombre binaire.
440 Or trouver un chemin hamiltonien
441 (comme étudié dans la partie précédente) dans un
442 $n$-cube revient à trouver un code
443 de Gray dans un mot de $n$-bits. Les compétences acquises lors du travail
444 sur les chemins hamiltoniens ont ainsi pu être réutilisées et approfondies.
445 Les résultats pratiques quant à l'utilisation de ces codes se sont cependant
446 révélés comme moins pertinents que l'utilisation de $n$ sorties.
447 Ceci a été valorisé dans les publications~\cite{cds12:ip,cds13:ij}.
451 \includegraphics[scale=0.5]{test.pdf}
453 \caption{Prédiction d'une force issue d'un flux d'air
454 le long d'un véhicule avec injecteurs}\label{fig:mems}
458 \subsubsection{Génération de nombres pseudo-aléatoires}
459 Au commencement de ce travail, notre équipe disposait d'un générateur de nombres
460 pseudo-aléatoires (PRNG)
461 basé sur une seule fonction dont nous avions prouvé la chaoticité
462 des itérations, à savoir la négation booléenne vectorielle. Cependant pour
463 réussir les tests statistiques dédiés aux PRNGs, il était nécessaire d'itérer
464 un grand nombre (arbitraire) de fois cette fonction entre deux
467 Avec la production d'une grande collection de fonctions à itérations chaotiques,
468 j'ai proposé de répondre à la question suivante: comment engendrer des fonctions
469 dont les itérations vont produire des nombres simulant correctement l'aléa.
470 J'ai d'abord caractérisé les fonctions dont les itérations produisent des nombres
471 selon une distribution uniforme~\cite{bcgr11:ip}. Pour cela il a fallu réécrire
472 l'algorithme de génération comme une marche aléatoire dans une partie du $n$-cube,
473 de se ramener à une chaîne de Markov puis d'utiliser la théorie élaborée sur ce sujet
474 pour conclure. Par la même occasion, nous avons démontré que certaines fonctions
475 chaotiques ne peuvent pas produire un aléa suivant une distribution uniforme.
476 La sortie est biaisée.
478 J'ai proposé ensuite des méthodes permettant de trouver de telles
479 fonctions en commençant par filtrer celles qui ne disposent pas
480 de cette caractéristique parmi toutes les fonctions chaotiques qui peuvent
481 être engendrées~\cite{bcgr11:ip}. J'ai démontré ensuite que supprimer
482 un cycle hamiltonien dans un $n$-cube permettait d'engendrer directement
483 des fonctions avec une telle caractéristique~\cite{chgw+14:oip}.
484 De plus, je me suis attaché à montrer l'importance
485 de l'équilibrage du chemin hamiltonien à enlever.
488 Les qualités statistiques des générateurs produits
489 ont été évalués avec succès~\cite{bcgw11:ip,chgw+14:onp,chgw+14:oip}
491 des batteries de tests telles que Die-Hard, NIST, TestU01.
493 Plus récemment, nous avons entrepris de trouver des bornes du temps d'arrêt
494 d'obtention d'une distribution uniforme d'un générateur
495 construit en enlevant un chemin hamiltonien équilibré dans un $n$-cube. Le travail
496 en collaboration avec Pr. P.-C. Heam du DISC
497 est en cours de soumission
498 dans un journal international.
500 Enfin j'ai été sollicité pour encadrer une thèse sur l'implantation
501 de générateurs de nombre pseudo-aléatoires à bases d'itérations
502 chaotiques sur des circuits logiques
503 programmables. J'ai commencé ce travail en encadrant une étude exhaustive
504 de toutes les instances d'implantations de cette classe.
505 Ce travail complet théorique et pratique est terminé aujourd'hui et
506 est en cours de soumission dans un journal international.
513 \subsubsection{Masquage d'information}\label{sub:ih}
515 La propriété de transitivité des fonctions chaotiques implique que l'on peut
516 atteindre tout point depuis le voisinage de n'importe quel point.
517 Lorsqu'on cherche à embarquer une marque dans un média,
518 si l'on souhaite de plus que celle-ci soit robuste, \textit{i.e.},
519 ne puisse pas être enlevée facilement, il paraît naturel d'embarquer
520 cette marque sur une grande partie du média.
521 L'utilisation de fonctions chaotiques
522 paraît alors judicieuse.
524 J'ai participé à la formalisation de la méthode de
525 marquage de médias~\cite{bcg11b:ip,bcg11:ij} et particularisé
526 ceci à des images numériques fournissant un
527 nouveau contexte pour l'étude théorique et mathématique d'algorithmes de marquage.
528 La chaos-sécurité a été introduite comme une nouvelle propriété
529 de tels algorithmes de marquage.
530 Nous avons de plus montré la robustesse d'un tel marquage dans les
531 domaines fréquentiels usuels (DWT ou DCT).
533 Des instances de ces algorithmes ont été présentées en sélectionnant de manière
534 pertinente les fonctions à itérer soit pour garantir une robustesse
535 élevée~\cite{bcfg12b:ip,bcfg+13:ip} soit pour masquer l'information dans le média
536 et être le moins détectable possible~\cite{bcfg12a:ip}.
538 D'autre méthodes de watermarking ont été investies,
539 particulièrement celles basées sur la Quantization Index Modulation (QIM), méthodes
540 étant supposées comme les plus robustes. Mes principales contributions
541 sur ce travail --en collaboration avec Dr R. Darazy de l'Université Antonine au Liban
542 et en co-encadrant le stage de M2 de Ahmad Bittar--,
544 d'intégrer ceci à du marquage de document PDF puis de
545 présenter ce problème comme un problème d'optimisation.
546 Grâce à une telle présentation nous avons pu trouver les paramètre optimaux
547 des méthodes QIM assurant à la fois robustesse et indétectabilité.
548 Le travail est en cours de soumission dans un journal international.
550 Lorsque l'objectif visé est l'indétectabilité, on parle de \emph{stéganographie}.
551 Ce domaine a été adressé en critiquant notamment les scénarios usuels d'évaluation
552 des algorithmes de stéganographie. J'ai proposé un cadre complémentaire permettant
553 d'évaluer ces schémas de masquage~\cite{fccg15:ip}.
554 Ceci se réalise en co-encadrant le doctorat de Y. Fadil.
556 J'ai de plus participé à l'élaboration de l'algorithme STABYLO~\cite{ccg15:ij}
558 stéganographie basé sur l'enfouissement de l'information dans les contours
559 présents dans une image et ilustré à la figure~\ref{fig:STABYLO}.
560 Ce travail est en collaboration avec Pr. R. Couturier.
561 Mes contributions ont principalement été la formalisation de l'algorithme et
562 son étude de complexité. Grâce a l'optimisation de cette dernière,
563 nous avons pu montrer
564 que cet algorithme présente un excellent compromis entre sécurité
565 fournie et complexité.
572 \includegraphics[scale=0.20]{lena512}
575 \begin{minipage}[b]{0.28\linewidth}
578 The skies they were ashen and sober;\linebreak
579 $\qquad$ The leaves they were crisped and sere—\linebreak
580 $\qquad$ The leaves they were withering and sere;\linebreak
581 It was night in the lonesome October\linebreak
582 $\qquad$ Of my most immemorial year;\linebreak
583 It was hard by the dim lake of Auber,\linebreak
584 $\qquad$ In the misty mid region of Weir—\linebreak
585 It was down by the dank tarn of Auber,\linebreak
586 $\qquad$ In the ghoul-haunted woodland of Weir.
591 \subfigure[Contours]{
592 \includegraphics[scale=0.20]{edge7}
594 \subfigure[Image avec msg.]{
595 \includegraphics[scale=0.20]{lena7}
599 \caption{Embarquement d'un message dans une image selon STABYLO}\label{fig:STABYLO}
604 \subsubsection{Les fonctions de hachage}\label{sub:hash}
605 Une fonction qui calcule une empreinte servant à identifier rapidement toute
606 donnée fournie en entrée est une fonction de hachage. On utilise ce genre
607 de fonctions dès qu'on veut comparer des éléments de grande taille car il
608 suffit de comparer leurs empreintes (généralement de taille plus réduite).
609 Une telle fonction doit induire de grandes variations dans l'empreinte
610 lorsque l'entrée varie même très peu. C'est l'effet avalanche. Cette
611 condition fait penser à la forte sensibilité aux conditions initiales
612 d'une fonction chaotique.
614 Forts de nos compétences sur les fonctions dont les itérations sont
615 chaotiques, nous avons proposé de nouvelles fonctions de hachage.
616 Celles-ci combinent des outils classiques utilisés dans les
618 usuelles et des itérations de systèmes dynamiques discrets étudiés
620 Nous avons prouvé que ces fonctions sont résistantes à la
621 seconde pré-image. Leur complexité, polynomiale en la taille
622 du message et la taille de l'empreinte, a été évaluée et correspond
623 à ce que l'on attend d'une telle fonction.
624 Nous avons de plus vérifié statistiquement le critère d'avalanche.
625 Ces résultats ont été valorisés dans les publications~\cite{bcg11:ip,bcg12:ij}.
630 \subsection{Application à la génomique}\label{sub:gen}
632 Ayant acquis des compétences sur certaines structures de mathématiques
633 discrètes (particulièrement théorie des graphes,
634 relations d'équivalence,\ldots), j'ai pu contribuer en bio-informatique
635 en les réappliquant notamment.
637 Une de mes premières pistes de travail a été de proposer une méthode automatique
638 de construction d'un ensemble de gènes communs (nommés core-génome)
639 à une famille de génomes.
640 La méthode s'appuie sur la construction du graphe de similarité
641 entre les gènes quotienté selon une relation d'équivalence pour en
642 réduire sa taille. Chaque gène est assimilé à son représentant de
643 classe dans chaque génome. Le core-génome se déduit comme l'intersection
644 de tous les génomes. Ceci a donné lieu aux
645 publications~\cite{acgs13:onp,akgcs+14:oip,acgm+14:ij}.
647 L'approche précédente souffrait de n'engendrer que des core-génomes de (trop)
648 petits cardinaux. J'ai contribué notamment
649 à l'amélioration de la méthode en proposant une étape d'optimisation issue
650 d'une adaptation discrète la méthode d'essaims particulaires~\cite{aagp+15:ip}.
651 D'autres travaux (dont la première étape est cette construction de
652 core-génome) ont été ensuite réalisés, principalement dans le but de
653 construire des arbres phylogénétiques de qualité~\cite{agcs+15:ip,aangc+15:ip}.
654 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}.
657 Tous ces travaux ont été réalisés en collaboration avec M. Salomon et en co-encadrant
658 le doctorat de B. Alkindy.
664 \section{Perspectives de recherche}
665 Les trois sections suivantes présentent quelques perspectives de recherche
666 autour de la thématique des systèmes dynamiques discrets.
670 \subsection{Les codes de Gray}
671 L'utilisation des codes de Gray dans une démarche d'apprentissage
672 (d'écoulement d'air ou de fonctions chaotiques) ne s'est pas révélée comme
673 concluante. Dans chacun des cas, la distance de Hamming entre deux
674 configurations voisines peut être très petite tandis que le chemin (dans le
675 cycle hamiltonien) qui les relie peut être long et ce même
676 pour des codes équilibrés.
677 Je propose de travailler sur ce problème discret en mesurant la qualité
678 du code de Gray à l'aide d'une fonction basée sur la longueur des chemins
679 (du cycle hamiltonien) entre les configurations voisines.
680 Je pense ainsi réduire ce problème à un problème d'optimisation et dégager
681 une démarche de génération, comme je l'ai fait en bio-informatique.
683 Jusqu'à présent, la production de codes de Gray équilibrés pour la génération
684 de nombres pseudo-aléatoires bute sur des problèmes d'explosion combinatoire:
685 les seuls algorithmes connus répondant à ce problème nécessitent a priori
686 plus de $10^{36}$ évaluations pour $n=8$.
687 Il n'est ainsi pas raisonnable de mettre en
688 pratique ce genre d'approche lorsque chacune de ces évaluations prend 1s.
690 se contenter de codes ``presque'' équilibrés , à défaut de pouvoir
691 trouver ceux qui seront équilibrés.
692 Je propose d'investiguer
693 dans cette thématique en exploitant des approches itératives permettant
694 d'obtenir des optimums locaux et trouver ainsi des codes presque équilibrés.
698 \subsection{Génération de nombres pseudo-aléatoires}
700 La démarche actuelle de génération de nombres pseudo-aléatoires
701 consiste à marcher dans une partie d'un $n$-cube en choisissant son chemin
702 à l'aide d'un générateur fourni en entrée. Or ces générateurs sont tous des
703 fonctions de $\{0,1\}^n$ dans lui-même. Cette approche
704 semble pouvoir se réécrire
705 comme un produit synchrone de deux automates.
706 L'intérêt d'une telle réécriture est qu'on pourrait exploiter
707 tous les résultats théoriques et pratiques déjà connus dans la communauté
709 Je pense investiguer cette voie pour améliorer notre approche,
710 s'affranchir, à terme, de tout autre générateur et améliorer la
711 connaissance à ce sujet.
712 Les propriété établies notamment sur les temps d'arrêt devraient être conservées.
713 Il restera à le prouver.
716 Jusqu'à présent, une seule expérimentation d'implantation de nos générateurs
717 sur des dispositifs physiques comme les FPGAs a été réalisée. Celle-ci
718 s'est faite automatiquement à l'aide de l'outil Matlab. Si le code engendré
719 sur le circuit est bien une implantation fidèle à la spécification,
720 il n'en est pas pour autant efficace: le nombre de bits générés par surface
721 est plutôt faible. Nous allons exploiter les meilleures démarches mises en
722 exergue lors de la rédaction d'un état de l'art exhaustif sur les PRNGs
723 implantés sur FPGA pour produire du code optimisé.
724 Je prévois de réaliser ceci dans la thèse de M. Bakiri, en cours.
726 Pour générer une fonction dont la matrice de Markov est doublement
727 stochastique, nous avons proposé principalement deux méthodes
728 (génération puis test, suppression de chemin hamiltonien dans un $n$-cube).
729 Ces deux méthodes ne passent pas à l'échelle, même pour des $n$ de petite taille.
730 Je pense attaquer ce problème algébriquement et en programmation logique avec
731 contraintes. Dans le premier cas, on peut remarquer qu'un matrice
732 composée de $1$ uniquement
733 en $(i,i+1)$ est une réponse triviale au problème. Je pense continuer l'étude
734 de ce genre de matrices et proposer une méthode plus générale de génération.
735 Je prévois de réaliser ce travail avec M. S. Contassot, Pr. à l'Université de Lorraine.
736 Le département DISC et l'équipe VESONTIO
737 a de fortes compétences en programmation logique avec
738 contraintes. J'ai déjà démontré que ce problème peut être soluble par cette
739 approche, sans avoir pour autant réussi à le faire.
740 Je prévois des collaborations avec l'équipe VESONTIO du DISC sur ce sujet.
743 Enfin, marcher dans une partie d'un $n$-cube est le modèle théorique que
744 nous avons établi pour notre classe de générateurs. On pourrait cependant
745 penser à ``sauter'' dans ce $n$-cube, c'est-à-dire modifier plusieurs bits
746 en une seule itération. J'ai commencé à étudier ce modèle avec les résultats
747 pratiques suivants: le nombre d'itérations suffisant pour un mélange
748 correct est plus petit que celui obtenu en marchant. De plus,
749 il diminue à mesure que $n$ augmente ce qui n'est pas le cas en marchant.
750 Pour l'instant, nous n'avons pas réussi à obtenir des bornes
751 du temps d'arrêt. Je propose d'investiguer aussi dans cette direction.
755 \subsection{Masquage d'information}
757 Concernant le marquage de données, plusieurs approches duales cohabitent pour
758 établir ou non la sécurité d'un algorithme
759 de cette classe: les probabilistes (stego-securité par ex.),
760 les métriques (chaos-securité par ex.),
761 les cryptographiques (mesure de fuite d'information).
762 Notre approche n'a pas encore été évaluée selon cette dernière métrique, ce
763 que je propose de faire.
765 Concernant l'indétectabilité, je propose de travailler à la fois sur
766 la stéganographie et sur la stéganalyse.
767 Nos expériences sur les schémas les plus efficaces de stéganographie
768 nous font penser qu'embarquer un message dans les contours comme cela l'a été fait pour
769 STABYLO est perfectible: on sait depuis qu'il existe des fonctions mathématiques
770 qui modélisent ces contours. Lorsqu'on modifie sans garde la valeur des bits de ces
771 contours, la ``continuité'' des fonctions qui les modélisent peut être perdue et
772 le message peut s'en trouver détectable. Que je sache, aucune approche de stéganographie
773 basée sur la continuité des fonctions de contours n'a jamais été proposée.
774 Je propose donc d'investiguer dans cette voie.
776 Les démarches de stéganalyse sont souvent composées de 2 étapes:
777 caractérisation puis classification.
778 On extrait au préalable une grande quantité des caractéristiques du média
779 puis on utilise une méthode de
780 classification basée sur celles-ci. La communauté voit souvent cette
781 seconde étape comme une boite noire et se concentre
782 sur la construction de l'ensemble des caractéristiques les plus discriminantes.
783 Autant que je sache, les méthodes algébriques
784 de réduction de domaine (analyse par composant principaux, SVD)
785 ont rarement été utilisées comme une étape intermédiaire entre la caractérisation et
786 la classification. Ces méthodes ont déjà été
787 appliquées avec succès lorsqu'elles sont combinées avec des méthodes
788 d'apprentissage, par exemple dans de la reconnaissance faciale.
789 Je propose d'étudier cette piste dans ce domaine.
790 Ceci se réalisera notamment au travers du doctorat de Y. Fadil.
796 \section{Insertion dans l'équipe de recherche}
798 La thématique principale de ma thèse et du post-doctorat qui a suivi
799 était la vérification de programmes par preuve automatique, soit de
800 la logique informatique.
801 Suite à mon recrutement dans l'équipe AND, mes recherches se sont réorientées
802 autour des SDDs et donc de l'analyse numérique plus généralement.
803 Ce défi de changement de thématique a été attaqué dès mon recrutement.
804 Les publications obtenues dans ces
805 domaines nouveaux pour moi ainsi que les éléments factuels suivants
806 permettent d'apprécier mon insertion au sein de cette équipe de recherche.
809 J'ai participé avec succès à deux appels à projets de la région de
812 \item \JFC{Projet region avec christophe}
813 \item appel 2015: j'ai participé à l'élaboration du
814 projet de \og capteurs multimédias collaboratifs: une approche
815 intégrée de la sécurité et de la robustesse\fg{} dont le porteur
816 est M. A. Mostefaoui. Nous avons obtenu le financement d'une bourse doctorale
817 pour la période d'oct. 2015--oct. 2018. Ce doctorat sera co-encadré par
818 M. A. Mostefaoui et moi-même.
821 J'ai établi des collaborations:
823 \item avec A. Richard CR CNRS du laboratoire
824 I3S (Nice)- UMR CNRS 7271 sur la thématique des SDDs et leurs
825 applications en Bio. Cela s'est traduit notamment avec
826 la publication~\cite{bcgr11:ip}.
828 \item avec R. Darazy de l'Université Antonine au Liban.
829 J'ai co-encadré trois stages de Master 2 recherche avec
830 des membres de cette université.
831 J'ai un article en cours de soumission résumant un travail en collaboration
832 avec un ancien étudiant et un enseignant chercheur de cette université.
834 \item avec Pr. S. Contassot-Vivier du LORIA (Nancy)- UMR CNRS 7503
835 sur la thématique des SDDs, de leur convergence dans les itérations
836 mixtes et de la générations de matrices de Markov doublement
837 stochastiques. Cela s'est traduit notamment avec
838 le rapport~\cite{BCVC10:ir}.
840 \item avec Pr. Y. Bailly et J.-C. Roy de l'équipe
841 MIE du département \'Energie de FEMTO-ST sur la thématique
842 de la prédiction d'écoulement d'un flux d'air le long d'un véhicule.
843 Cela s'est traduit notamment avec
844 les publications~\ref{cds13:ij,cds12:ip}.
850 \item au workshop \og Théorie des réseaux booléens et ses applications en
851 biologie\fg{} à Nice en novembre 2014 (20 participants);
852 \item à la journée \og Advances in Mobile Technologies Day\ fg{}
853 organisée par l'Université Antonine au Liban en mai 2013 (10 participants);
854 \item au Séminaire MDSC (Modèles Discrets pour les Systèmes Complexes)
855 du laboratoire I3S sur le sujet \og Efficiently dealing with
856 SMT-LIB provers in software verification\fg{}
857 en décembre 2007 (30 participants).
860 J'ai co-organisé avec J. Bahi et C. Guyeux
861 \og The First Workshop on Information Hiding Techniques
862 for Internet Anonymity and Privacy (IHTIAP) \fg{} à Venise en juin 2012
864 \url{http://www.iaria.org/conferences2012/IHTIAP.html}.
865 Le comité de programme était composé de 18 chercheurs internationaux
866 (dont je faisais aussi partie).
867 Il s'est déroulé sur 1/2 journée et 5 chercheurs ont présenté leurs travaux.
868 Le taux d'acceptation des articles a été de 41\%.
871 J'ai fait partie des comités de programme des conférences \og int. conf. on Evolving Internet \fg{}, (2013, 2014)
874 J'ai rédigé des rapports de relecture pour les journaux internationaux
877 \item The computer Journal (2);
878 \item Springer Multimedia Tool and application (1);
879 \item Springer Annals in Telecommunication (1);
881 et pour les conférences suivantes:
883 \item MAJECSTIC (2005 (2), 2007 (2));
884 \item ZB 2007 (1), A-BZ 2008 (1);\JFC{A verifier}
885 \item Evolving Internet \fg{}, (2012 (2), 2013 (2), 2014 (1));
886 \item ICCVE 2014 (1).\JFC{A verifier}
889 Membre du GDR codes et cryptographie, j'ai
890 participé aux Journées Codes et Stéganographie en 2012 (Rennes)
891 où j'ai présenté \og Steganography: secure and robust algorithms \fg{} et en 2013 (Paris).
898 \section{Encadrement et co-encadrement d'étudiants}
900 \subsection{Thèse d'université}
905 (à hauteur de 40\%) avec Michel Salomon (40\%) et
906 Jacques M. Bahi (20\%) le doctorat de Bassam Alkindy
907 sur les combinaisons d'approches pour la prédiction de l'évolution génomique.
908 Le doctorat a commencé en septembre 2012 et devrait être soutenu en
910 Ce travail de thèse a donné lieu à 6 publications dans des conférences
912 \item (à hauteur de 50\%) avec Christophe Guyeux (50\%)
913 le doctorat de Youssra Fadil
915 l'étude du comportement des outils d'intelligence artificielle
916 face à des dynamiques complexes.
917 Le doctorat a commencé en décembre 2013 et devrait être soutenu en
919 Ce travail de thèse a donné lieu à 1 publication dans une conférence
922 \item (à hauteur de 50\%) avec Christophe Guyeux (50\%)
923 le doctorat de Mohamed Bakiri
925 l'implémentation matérielle de générateurs de nombres pseudo-aléatoires basés sur les itérations chaotiques.
926 Le doctorat a commencé en septembre 2014 et devrait être soutenu en
928 Ce travail de thèse a donné lieu à 1 publication dans un journal international
929 en cours de soumission.
933 \subsection{Master 2 recherche}
938 \item (à hauteur de 34\%) avec Raphael Couturier (33\%) et
939 Rony Darazi -- Université Antonine au Liban--(33\%)
940 le stage de recherche de Master 2 de Ahmad Bittar
943 Steganography in PDF documents based on Unprintable Control ASCII Codes.
944 Le stage a commencé le 01 mai 2013 et a été soutenu le 30 septembre 2013.
945 Ce travail de Master a donné lieu à 1 publication dans un journal international
946 en cours de soumission (en révision mineure).
947 \item (à hauteur de 80\%) avec
948 Talar Atechian -- Université Antonine au Liban--(20\%)
949 le stage de recherche de Master 2 de Hussein Nasser
952 Critical Analysis of Distributed Algorithm for Sensor
953 Network Lifetime Maximization.
954 Le stage a commencé le 01 avril 2014 et a été soutenu le 31 août 2014.
957 \item (à hauteur de 80\%) avec
958 Talar Atechian -- Université Antonine au Liban--(20\%)
959 le stage de recherche de Master 2 de Khaled Daher
960 sur la désynchronisation du calcul d'optimisation de la durée de vie
961 d'un réseau de capteurs.
962 Le stage a commencé le 01 avril 2015 et sera soutenu le 31 août 2015.
967 \section{Participation à des tâches d'intérêt collectif}
969 Depuis septembre 2000, je suis titulaire à l'Université de Franche-Comté,
970 soit sur un poste de PrCe (de 2000 à 2008, sauf l'année 2006-2007) soit sur
971 un poste de MdC. J'ai assuré un grand nombre d'enseignements de la première
972 année de licence ou de DUT jusqu'en seconde année de Master.
974 recrutement comme MdC, j'ai recentré mes enseignements autour
975 de mes thématiques de recherche, à savoir essentiellement les
976 mathématiques discrètes.
977 La répartition moyenne de mes enseignements
978 sur les quatre dernières années est la suivante:
980 \item 6\% en le master Informatique Mobile et Répartie (UFR STGI),
982 \og Modélisation et d'Evaluation des Systèmes Informatiques \fg{}. Ce sont des
983 promotions d'une vingtaine d'étudiants à chaque fois;
984 \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
985 promotions d'une vingtaine d'étudiants à chaque fois;
986 \item 15\% en encadrement de projets tutorés ou de stage;
987 \item 28\% en DUT d'informatique dans l'UE de
988 \og conception et développement d'applications mobiles\fg{};
989 \item 44\% en DUT d'informatique dans les UEs de
990 \og mathématiques discrètes \fg{} et
992 \og modélisations mathématiques \fg{}.
995 J'ai aussi la responsabilité de toutes les UE données ci-dessus et
996 suis de plus le coordinateur des enseignements de mathématiques
997 au département d'informatique de l'IUT BM.
998 J'ai participé à ce titre à l'élaboration des parties de mathématiques du
999 PPN du DUT d'informatique, à Dijon en 2011 et Orléans en 2012.
1000 Depuis septembre 2014, je suis le responsable du parcours TeProw
1001 de la LP CAM localisée
1002 à l'IUT BM. Cette licence
1003 a aussi un parcours à l'UFR ST. Je coordonne toute l'organisation
1004 de cette licence avec mon collègue de Besançon.
1007 J'ai été membre élu du conseil d'institut de l'IUT BM
1008 de novembre 2010 à novembre 2014. A ce titre j'ai participé à la vie administrative de l'IUT,
1009 aux commissions de recrutement d'enseignants et d'enseignants-chercheurs\ldots
1010 Depuis septembre 2014, je suis élu au conseil du département d'informatique
1013 Je suis régulièrement membre de jury des épreuves TIPE, épreuves communes
1014 à 90 concours d'ingénieurs (sessions 2012 et 2015) et fournis
1015 à chaque session des sujets scientifiques pour l'épreuve.
1021 \section{Publications après la thèse}\label{sec:publi}
1022 Le tableau de la figure~\ref{fig:bilan} donné
1023 ci dessous synthéthise les références détaillées ci-après.
1028 \begin{tabular}{|c|c|c|c|c|}
1030 %& \multicolumn{2}{|c|}{Internationaux} & {Nationaux} & \\
1032 & Journaux & Conférences &
1033 Conférences & Divers\\
1034 & internationaux & internationales &
1038 Pendant le doctorat &
1043 \cite{cddg+04:ip,CGK05}
1047 \cite{cdgr04:onp,cg04:np}
1051 \cite{couchot04:onp}
1059 \cite{BCDG07,CouchotD07IFM,cgs09:ip,couchot07FTP,couchot07cade}
1075 \cite{aangc+15:ip,aagp+15:ip,acgm+14:ij,
1076 akgcs+14:oip,agcs+15:ip}
1091 \cite{bcg12:ij,bcg11:ij,bcgs12:ij,ccg15:ij,cds13:ij}
1101 \cite{bcfg+13:ip,bcfg12a:ip,bcfg12b:ip,bcg11:ip,bcg11b:ip}
1109 \cite{acgs13:onp,BCVC10:ir,chgw+14:onp,Cou10:ir}
1120 \cite{bcgr11:ip,bcgw11:ip,cds12:ip,chgw+14:oip,fccg15:ip}
1137 \caption{Bilan synthétique des publications}\label{fig:bilan}
1142 \subsection{Journaux internationaux avec comité de sélection}
1144 \begin{thebibliography}{CHG{\etalchar{+}}14b}
1147 \addtocounter{\@listctr}{6}
1151 Jacques Bahi, Jean-Fran\c{c}ois Couchot, and Christophe Guyeux.
1152 \newblock Quality analysis of a chaotic proven keyed hash function.
1153 \newblock {\em International Journal On Advances in Internet Technology},
1158 Jacques Bahi, Jean-Fran\c{c}ois Couchot, and Christophe Guyeux.
1159 \newblock Steganography: a class of secure and robust algorithms.
1160 \newblock {\em The Computer Journal}, 55(6):653--666, 2012.
1163 Jacques Bahi, Jean-Fran\c{c}ois Couchot, Christophe Guyeux, and Michel Salomon.
1164 \newblock Neural networks and chaos: Construction, evaluation of chaotic
1165 networks, and prediction of chaos with multilayer feedforward network.
1166 \newblock {\em Chaos, An Interdisciplinary Journal of Nonlinear Science},
1167 22(1):013122--1 -- 013122--9, March 2012.
1173 Jean-Fran\c{c}ois Couchot, Rapha\"el Couturier, and Christophe Guyeux.
1174 \newblock {STABYLO}: {STeganography with Adaptive, Bbs, and binarY embedding at
1176 \newblock {\em Annals of Telecommunications}, 2015.
1177 \newblock Available online. Paper version to appear.
1181 Jean-Fran\c{c}ois Couchot, Karine Deschinkel, and Michel Salomon.
1182 \newblock Active {MEMS}-based flow control using artificial neural network.
1183 \newblock {\em Mechatronics}, 23(7):898--905, October 2013.
1184 \newblock Available online. Paper version to appear.
1186 \end{thebibliography}
1188 \subsection{Conférences internationales avec comité de sélection}
1190 \begin{thebibliography}{CHG{\etalchar{+}}14b}
1192 \addtocounter{\@listctr}{11}
1195 \bibitem{aangc+15:ip}
1196 Bassam Alkindy, Huda Al'Nayyef, Christophe Guyeux, Jean-Fran\c{c}ois Couchot,
1197 Michel Salomon, and Jacques Bahi.
1198 \newblock Improved core genes prediction for constructing well-supported
1199 phylogenetic trees in large sets of plant species.
1200 \newblock In {\em IWBBIO 2015, 3rd Int. Work-Conf. on Bioinformatics and
1201 Biomedical Engineering, Part I}, volume 9043 of {\em LNCS}, pages 379--390,
1202 Granada, Spain, April 2015.
1204 \bibitem{acgm+14:ij}
1205 Bassam Alkindy, Jean-Fran\c{c}ois Couchot, Christophe Guyeux, Arnaud Mouly,
1206 Michel Salomon, and Jacques Bahi.
1207 \newblock Finding the core-genes of chloroplasts.
1208 \newblock In {\em ICBBS 2014, 3rd Int. Conf. on Bioinformatics and Biomedical
1209 Science}, number 4(5) in IJBBB, Journal of Bioscience, Biochemistery, and
1210 Bioinformatics, pages 357--364, Copenhagen, Denmark, June 2014.
1212 \bibitem{akgcs+14:oip}
1213 Bassam Alkindy, Christophe Guyeux, Jean-Fran\c{c}ois Couchot, Michel Salomon,
1215 \newblock Gene similarity-based approaches for determining core-genes of
1217 \newblock In {\em BIBM14, IEEE Int. Conf. on Bioinformatics and Biomedicine},
1218 Belfast, United Kingdom, November 2014.
1219 \newblock Short paper.
1221 \bibitem{agcs+15:ip}
1222 Bassam Alkindy, Christophe Guyeux, Jean-Fran\c{c}ois Couchot, Michel Salomon,
1223 Christian Parisod, and Jacques Bahi.
1224 \newblock Hybrid genetic algorithm and lasso test approach for inferring well
1225 supported phylogenetic trees based on subsets of chloroplastic core genes.
1226 \newblock In {\em AlCoB 2015, 2nd Int. Conf. on Algorithms for Computational
1227 Biology}, volume~* of {\em LNCS/LNBI}, pages ***--***, Mexico City, Mexico,
1228 August 2015. Springer.
1229 \newblock To appear in the LNCS/LNBI series.
1231 \bibitem{aagp+15:ip}
1232 Reem Alsrraj, Bassam Alkindy, Christophe Guyeux, Laurent Philippe, and
1233 Jean-Fran\c{c}ois Couchot.
1234 \newblock Well-supported phylogenies using largest subsets of core-genes by
1235 discrete particle swarm optimization.
1236 \newblock In {\em CIBB 2015, 12th Int. Meeting on Computational Intelligence
1237 Methods for Bioinformatics and Biostatistics}, pages ***--***, Naples, Italy,
1239 \newblock To appear.
1242 \bibitem{bcfg12a:ip}
1243 Jacques Bahi, Jean-Fran\c{c}ois Couchot, Nicolas Friot, and Christophe Guyeux.
1244 \newblock Application of steganography for anonymity through the internet.
1245 \newblock In {\em IHTIAP'2012, 1-st Workshop on Information Hiding Techniques
1246 for Internet Anonymity and Privacy}, pages 96--101, Venice, Italy, June 2012.
1248 \bibitem{bcfg12b:ip}
1249 Jacques Bahi, Jean-Fran\c{c}ois Couchot, Nicolas Friot, and Christophe Guyeux.
1250 \newblock A robust data hiding process contributing to the development of a
1252 \newblock In {\em INTERNET'2012, 4-th Int. Conf. on Evolving Internet}, pages
1253 71--76, Venice, Italy, June 2012.
1255 \bibitem{bcfg+13:ip}
1256 Jacques Bahi, Jean-Fran\c{c}ois Couchot, Nicolas Friot, Christophe Guyeux, and
1258 \newblock Quality studies of an invisible chaos-based watermarking scheme with
1260 \newblock In {\em IIHMSP'13, 9th Int. Conf. on Intelligent Information Hiding
1261 and Multimedia Signal Processing}, pages 547--550, Beijing, China, October
1265 Jacques Bahi, Jean-Fran\c{c}ois Couchot, and Christophe Guyeux.
1266 \newblock Performance analysis of a keyed hash function based on discrete and
1267 chaotic proven iterations.
1268 \newblock In {\em INTERNET 2011, the 3-rd Int. Conf. on Evolving Internet},
1269 pages 52--57, Luxembourg, Luxembourg, June 2011.
1270 \newblock Best paper award.
1273 Jacques Bahi, Jean-Fran\c{c}ois Couchot, and Christophe Guyeux.
1274 \newblock Steganography: a class of algorithms having secure properties.
1275 \newblock In {\em IIH-MSP-2011, 7-th Int. Conf. on Intelligent Information
1276 Hiding and Multimedia Signal Processing}, pages 109--112, Dalian, China,
1281 Jacques Bahi, Jean-Fran\c{c}ois Couchot, Christophe Guyeux, and Adrien Richard.
1282 \newblock On the link between strongly connected iteration graphs and chaotic
1283 boolean discrete-time dynamical systems.
1284 \newblock In {\em FCT'11, 18th Int. Symp. on Fundamentals of Computation
1285 Theory}, volume 6914 of {\em LNCS}, pages 126--137, Oslo, Norway, August
1289 Jacques Bahi, Jean-Fran\c{c}ois Couchot, Christophe Guyeux, and Qianxue Wang.
1290 \newblock Class of trustworthy pseudo random number generators.
1291 \newblock In {\em INTERNET 2011, the 3-rd Int. Conf. on Evolving Internet},
1292 pages 72--77, Luxembourg, Luxembourg, June 2011.
1295 Fabrice Bouquet, Jean-Fran\c{c}ois Couchot, Fr\'ed\'eric Dadeau, and Alain
1297 \newblock Instantiation of parameterized data structures for model-based
1299 \newblock In Jacques Julliand and Olga Kouchnarenko, editors, {\em B'2007, the
1300 7th Int. B Conference}, volume 4355 of {\em LNCS}, pages 96--110, Besancon,
1301 France, January 2007. Springer.
1303 \bibitem{CouchotD07IFM}
1304 Jean-Fran\c{c}ois Couchot and Fr\'ed\'eric Dadeau.
1305 \newblock Guiding the correction of parameterized specifications.
1306 \newblock In {\em IFM'07, 6th Int. Conf. on Integrated Formal Methods}, volume
1307 4591 of {\em LNCS}, pages 176--194, Oxford, UK, July 2007. Springer.
1311 Jean-Fran\c{c}ois Couchot, Karine Deschinkel, and Michel Salomon.
1312 \newblock Suitability of artificial neural network for {MEMS}-based flow
1314 \newblock In Julien Bourgeois and Michel de~Labachelerie, editors, {\em dMEMS
1315 2012, Workshop on design, control and software implementation for distributed
1316 MEMS}, pages 1--6, Besan\c{c}on, France, April 2012. IEEE CPS.
1320 Jean-Fran\c{c}ois Couchot, Alain Giorgetti, and Nicolas Stouls.
1321 \newblock {G}raph {B}ased {R}eduction of {P}rogram {V}erification {C}onditions.
1322 \newblock In Hassen Sa\"{i}di and N.~Shankar, editors, {\em AFM'09, {A}utomated
1323 {F}ormal {M}ethods (colocated with {CAV}'09)}, pages 40--47, Grenoble,
1324 France, 2009. ACM Press.
1326 \bibitem{chgw+14:oip}
1327 Jean-Fran\c{c}ois Couchot, Pierre-Cyrille H\'eam, Christophe Guyeux, Qianxue
1328 Wang, and Jacques Bahi.
1329 \newblock Pseudorandom number generators with balanced gray codes.
1330 \newblock In {\em Secrypt 2014, 11th Int. Conf. on Security and Cryptography},
1331 pages 469--475, Vienna, Austria, August 2014.
1334 \bibitem{couchot07FTP}
1335 Jean-Fran\c{c}ois Couchot and T.~Hubert.
1336 \newblock A graph-based strategy for the selection of hypotheses.
1337 \newblock In {\em FTP'07, Int. Workshop on First-Order Theorem Proving},
1338 Liverpool, UK, September 2007.
1340 \bibitem{couchot07cade}
1341 Jean-Fran\c{c}ois Couchot and S.~Lescuyer.
1342 \newblock Handling polymorphism in automated deduction.
1343 \newblock In {\em CADE'07, 21st Int. Conf. on Automated Deduction}, volume 4603
1344 of {\em LNCS}, pages 263--278, Bremen, Germany, July 2007. Springer.
1348 Yousra~Ahmed Fadil, Jean-Fran\c{c}ois Couchot, Rapha\"el Couturier, and
1350 \newblock Steganalyzer performances in operational contexts.
1351 \newblock In {\em IIH-MSP 2015, 11th Int. Conf. on Intelligent Information
1352 Hiding and Multimedia Signal Processing}, pages ***--***, Adelaide,
1353 Australia, September 2015.
1354 \newblock To appear.
1356 \end{thebibliography}
1358 \subsection{Communications orales invitées}
1363 \item au Workshop \og Théorie des réseaux booléens et ses applications en biologie\fg{}
1364 à Nice en novembre 2014;
1366 \item à la journée \og Advances in Mobile Technologies Day\fg{} par l'Université Antonine (Liban) en mai 2013;
1368 \item au Séminaire MDSC (Modèles Discrets pour les Systèmes Complexes)
1369 du laboratoire I3S sur le sujet \og Efficiently dealing with SMT-LIB provers in software verification\fg{} en décembre 2007.
1372 \subsection{Communications diverses}
1373 \begin{thebibliography}{CHG{\etalchar{+}}14b}
1376 \addtocounter{\@listctr}{31}
1379 \bibitem{acgs13:onp}
1380 Bassam Alkindy, Jean-Fran\c{c}ois Couchot, Christophe Guyeux, and Michel
1382 \newblock Finding the core-genes of chloroplast species.
1383 \newblock Journ\'ees SeqBio 2013, Montpellier, November 2013.
1389 J.~M. Bahi, S.~Contassot-Vivier, and J.-F. Couchot.
1390 \newblock Convergence results of combining synchronism and asynchronism for
1391 discrete-state discrete-time dynamic network.
1392 \newblock Research Report RR2010-02, LIFC - Laboratoire d’{I}nformatique de
1393 l'{U}niversit\'{e} de {F}ranche {C}omt\'{e}, May 2010.
1398 \newblock Formal {C}onvergence {P}roof for {D}iscrete {D}ynamical {S}ystems.
1399 \newblock Research Report RR2010-03, LIFC - Laboratoire d’{I}nformatique de
1400 l'{U}niversit\'{e} de {F}ranche {C}omt\'{e}, May 2010.
1402 \bibitem{chgw+14:onp}
1403 Jean-Fran\c{c}ois Couchot, Pierre-Cyrille H\'eam, Christophe Guyeux, Qianxue
1404 Wang, and Jacques Bahi.
1405 \newblock Traversing a n-cube without balanced hamiltonian cycle to generate
1406 pseudorandom numbers.
1407 \newblock 15-th Mons Theoretical Computer Science Days (15e Journ\'ees
1408 Montoises d'Informatique Th\'eorique), Nancy, France, September 2014.
1411 \end{thebibliography}
1419 % \section{Avis du directeur de l'Equipe}\label{sec:avis:directeur}
1421 %\bibliographystyle{plain}
1422 %\bibliography{abbrev,biblioand}