X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/ab856c6a43de1e2a3bdbc0361e1da1e4da76a3d1..28b18f7c0f58e36c0c2ed675a8bcc3c38c3aee96:/demandeInscription/synthese.tex?ds=sidebyside diff --git a/demandeInscription/synthese.tex b/demandeInscription/synthese.tex index a9ba499..2255df8 100755 --- a/demandeInscription/synthese.tex +++ b/demandeInscription/synthese.tex @@ -1,4 +1,4 @@ -\documentclass[a4paper,french,11pt]{article} +\documentclass[a4paper,french,12pt]{article} %\usepackage{hyperlatex} \usepackage[utf8]{inputenc} \usepackage[T1]{fontenc} @@ -31,6 +31,7 @@ \newcommand{\JFC}[1]{\begin{color}{green}\textit{#1}\end{color}} +\newcommand{\etalchar}[1]{$^{#1}$} % %\lstset{% general command to set parameter(s) @@ -44,7 +45,6 @@ %showstringspaces=false} % no special string spaces - \usepackage{hyperref} \pdfcompresslevel=9 \hypersetup{ @@ -58,9 +58,9 @@ %bookmarks=true, %créé des signets pour Acrobat bookmarksopen=true, %si les signets Acrobat sont créés, %les afficher complÚtement. - pdftitle={Cours d'algèbre et de géométrie}, %informations apparaissant dans - pdfauthor={Jean-Fran\c{c}ois Couchot, Christophe Guyeux}, %dans les informations du document - pdfsubject={Algèbre et géométrie} %sous Acrobat. + 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. } @@ -80,7 +80,7 @@ %\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}} @@ -89,15 +89,16 @@ %\lstset{language=C} \maketitle -\section{Curriculum vit{\ae} (1 page).} +\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} +%\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 @@ -117,7 +118,7 @@ Maîtrise d'informatique, mention B (UFC). logico-ensemblistes}. Major de Promotion, mention TB. \item{\bf{avril 06~:}} Doctorat en informatique au Laboratoire d'Informatique -de l'Université de Franche Comté (LIFC EA 4269), +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} @@ -128,76 +129,988 @@ mention très honorable. \item{\bf{95-00~:}} Enseignant en mathématiques dans le secondaire, successivement à Aurillac(15), Beaune(21), Belfort(90) et Montbéliard(25). -\item{\bf{sept. 00-06~:}} PrCe $71^{eme}$ section, Unité de Formation +\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^{eme}$ section, UFR SLHS à l'UFC. -\item{\bf{sept. 08-\ldots~:}} Maître de Conférences $27^{eme}$ section, IUT de Belfort-Montbéliard, dpt. informatique (UFC). -\item{\bf{sept. 10-14\ldots~:}} \'Elu au Conseil d'Institut de l'IUT de Belfort-Montbéliard. +\item{\bf{sept. 07-08~:}} PrCe $71^{ème}$ section, UFR SLHS à l'UFC. +\item{\bf{sept. 08-\ldots~:}} Maître de Conférences $27^{ème}$ section, IUT de Belfort-Montbéliard (IUT BM), au département d'informatique (UFC). +\item{\bf{sept. 11-14\ldots~:}} \'Elu au Conseil d'Institut de l'IUT BM. \end{itemize} -\section{Nom et type de l'équipe de recherche (1 page).} +\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. -L'avis du directeur de l'équipe et du directeur de l'école doctorale sont -annexés à cette synthèse. -\JFC{joindre l'avis de Raphale, d'Olga de Nicolas et de PH. Lutz} -\newpage -\section{Résumé (1 page)} de la thématique de la thèse d'université (ou d'Etat le cas échéant) -et liste des publications auxquelles elle a donné lieu ; +\subsection{Avis du directeur de l'équipe}\label{sec:avis:directeur:equipe} + +\subsection{Avis du directeur de recherche}\label{sec:avis:directeur:recherhce} + +\subsection{Avis du directeur de l'école doctorale}\label{sec:avis:directeur:spim} + \newpage -\section{Exposé des recherches réalisées au cours de la période postdoctorale (5 pages maximum)} +\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} +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]{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[CDD{\etalchar{+}}04]{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]{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]{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]{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. + +\end{thebibliography} + + + + + + + + + + + + + -(ou post-DEA pour les candidats autorisés à présenter leur demande sans -thèse), en identifiant les grandes thématiques de recherche, la démarche suivie et les -retombées en terme de publications et/ou de brevets ; \newpage -\section{Perspectives de recherche (1 à 2 pages maximum)} +\section{Exposé des recherches réalisées au cours de la période postdoctorale} + +Entre avril 2006 et aujourd'hui, les recherches réalisées ont concerné plusieurs domaines synthétisés ci-après. Le premier travail (Sec.~\ref{sub:verif}) +est une suite directe des travaux de thèse. Suivent six sections +(de la Sec.~\ref{sub:sdd} à la Sec.~\ref{sub:hash}) sur les systèmes +dynamiques discrets et leurs applications, thématique +pour laquelle j'ai été recruté dans l'équipe AND du département +DISC. Enfin la section~\ref{sub:gen} présente comment j'ai réinvesti le +domaine de la bio-informatique à l'aide de compétences connexes. +Ces travaux ont été valorisés par des publications dont les références sont données. + +\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{Convergence de systèmes dynamiques discrets}\label{sub:sdd} + +Un système dynamique discret (SDD) est une fonction $f$ +du $n$-cube ($\{0,1\}^n$) dans lui même et un mode opératoire +(parallèle, unaire, généralisé) qui peut être itéré +en synchrone ou en asynchrone. +%Ils ont été étudiés à de maintes reprises ~\cite{Rob95,Bah00,bcv02}. +Pour chacun de ces modes, il existe des critères (suffisants) de convergence +globale ou locale, souvent basés sur le fait que $f$ +est un opérateur contractant dans un espace. + +Les modes asynchrones ont une dynamique avec plus de liberté +puisqu'ils autorisent chaque élément à modifier sa valeur avant +de connaître les valeurs des autres éléments dont il dépend. +Cependant, lorsque les calculs à effectuer sur certains n{\oe}uds +sont coûteux en temps et/ou que les temps de communication sont élevés, +ces modes peuvent présenter une convergence plus rapide que le cas synchrone. + +J'ai formalisé le mode des +\emph{itérations mixes} (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 mixes 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 mixes à 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 est simple à vérifier +pratiquement pour le mode synchrone. +C'est beaucoup plus complexe lorsqu'on traite des itérations asynchrones +et mixes prenant de plus en compte les délais. +Des méthodes de simulation basées sur des stratégies et des délais générés aléatoirement avaient déjà été présentées. +Cependant, comme ces implantations ne sont pas exhaustives, elles ne sont intéressantes que lorsqu'elles fournissent un contre-exemple. +Lorsqu'elles exhibent une convergence, +cela ne permet que de donner une intuition de convergence, pas une preuve. +Autant que je sache, aucune démarche de preuve formelle automatique +de convergence n'avait jamais été établie. + + +J'ai démontré qu'on peut simuler +des SDDs selon tous les modes pour établir +formellement leur convergence (ou pas). +Cette simulation est basée sur l'outil SPIN de \emph{Model-Checking}. +Pour traiter le problème d'explosion +combinatoire, les outils de cette classe +appliquent des méthodes d'ordre partiel, d'abstraction, +de quotientage selon une relation d'équivalence. +J'ai présenté pour cela une démarche de traduction d'un SDD +dans SPIN. +J'ai énoncé puis prouvé ensuite la correction et la complétude de la démarche. +Des données pratiques comme la complexité et des synthèses d'expérimentation +ont aussi été fournies. +Ceci a été synthétisé dans~\cite{Cou10:ir} + + +\subsection{Construction de fonctions chaotiques} +Je me suis intéressé ensuite à l'étude du problème dual +de l'étude de divergence d'un SDD. +Le Pr. C. Guyeux de l'équipe AND a proposé dans sa thèse en 2010 +une caractérisation des fonctions $f$ de $\{0,1\}^n$ dans lui-même +dont les itérations sont chaotiques selon Devanney pour un mode donné: +il est nécessaire et suffisant que son graphe des itérations soit +fortement connexe. +J'ai proposé plusieurs méthodes de construction de +fonctions ayant de tels graphes d'itérations~\cite{bcgr11:ip,chgw+14:onp}. + +Dans la première~\cite{bcgr11:ip}, +l'algorithme enlève des arcs et vérifie ensuite que +la forte connexité est maintenue. +Même si cet algorithme retourne toujours des fonctions dont le graphe +des itérations est fortement connexe, il n'en est pas pour autant efficace +car il nécessite une vérification à posteriori de la +forte connexité sur le graphe entier composé de $2^n$ sommets. +La seconde méthode propose une solution à ce problème en présentant +des conditions suffisantes sur un graphe à $n$ sommets +qui permettent d'obtenir des graphes d'itérations fortement connexes. +Ce théorème a aussi été prouvé dans~\cite{bcgr11:ip} +et des instanciations effectives +ont été produites. +Une troisième méthode~\cite{chgw+14:onp} s'appuie sur les codes +de Gray, ou de manière équivalente sur les cycles hamiltoniens du graphe des +itérations. +% : un cycle qui visite chaque n{\oe}ud exactement une fois est un +% \emph{cycle hamiltonien}. +%La démarche consiste à enlever du graphe un de ses cycles hamiltoniens dont +%la démarche de génération est un problème connu. + +Ces méthodes ont permis d'étendre à l'infini la classe des fonctions +dont les itérations sont chaotiques. + + +\subsection{Apprentissage par réseaux neuronaux} +Nous disposons grâce aux travaux présentés à la section précédente d'un grand +nombre de fonctions dont les itérations sont chaotiques. +Nous avons entrepris d'étudier ces itérations et plus particulièrement leur +apprentissage par un réseau de neurones. +J'ai notamment pu contribuer à montrer pratiquement qu'il +est très difficile (voir impossible) de les prédire +à l'aide d'outils d'intelligence artificielle~\cite{bcgs12:ij}. + + +Nous nous sommes attaqués parallèlement +à un problème physique d'optimisation de +l'écoulement d'un flux d'air le long d'un véhicule. +Ce flux peut être modifié si l'on active des injecteurs d'air placés +par exemple sur le becquet du véhicule. +Le flux d'air peut être modélisé à l'aide d'équations de Navier-Stokes +dont on ne connaît pas de méthode analytique de résolution. +De plus, le nombre de Reynolds calculé dans cette situation fait apparaître +que le régime est extrêmement turbulent, donc difficile à prévoir. +Nous avons souhaité +continuer nos expériences d'apprentissage à l'aide +de réseau de neurones dans ce contexte. + Il est apparu comme judicieux de mémoriser les configurations +représentant l'état des actionneurs à l'aide de nombres binaires. +De plus les codes de Gray (dont deux mots adjacents ne diffèrent que d'un +bit) se sont présentés comme une des manières de mémoriser les sorties du +réseau de neurones comme un seul nombre binaire. +Quand on sait que trouver un chemin hamiltonien (comme étudié dans la partie précédente) dans un +$n$-cube revient à trouver un code +de Gray dans un mot de $n$-bits. Les compétences acquises lors du travail +sur les chemins hamiltoniens ont ainsi pu être réutilisées et approfondies. +Les résultats pratiques quant à l'utilisation de ces codes se sont cependant +révélés comme moins pertinents que l'utilisation de $n$ sorties. +Ceci a été valorisé dans les publications~\cite{cds12:ip,cds13:ij}. + +\subsection{Génération de nombres pseudo-aléatoires} +Au commencement de ce travail, notre équipe disposait d'un générateur de nombres +pseudo-aléatoires (PRNG) +basé sur une seule fonction dont nous avions prouvé la chaoticité +des itérations, à savoir la négation booléenne vectorielle. Cependant pour +réussir les tests statistiques dédiés aux PRNGs, il était nécessaire d'itérer +un grand nombre (arbitraire) de fois cette fonction entre deux +sorties. + +Avec la production d'une grande collection de fonctions à itérations chaotiques, +j'ai proposé de répondre à la question suivante: comment engendrer des fonctions +dont les itérations vont produire des nombres simulant correctement l'aléa. +J'ai d'abord caractérisé les fonctions dont les itérations produisent des nombres +selon une distribution uniforme~\cite{bcgr11:ip}. Pour cela il a fallu réécrire +l'algorithme de génération comme une marche aléatoire dans une partie du $n$-cube, +de se ramener à une chaîne de Markov puis d'utiliser la théorie élaborée sur ce sujet +pour conclure. Par la même occasion, nous avons démontré que certaines fonctions +chaotiques ne peuvent pas produire un aléa suivant une distribution uniforme. +La sortie est biaisée. + +J'ai proposé ensuite des méthodes permettant de trouver de telles +fonctions en commençant par filtrer celles qui ne disposent pas +de cette caractéristique parmi toutes les fonctions chaotiques qui peuvent +être engendrées~\cite{bcgr11:ip}. J'ai démontré ensuite que supprimer +un cycle hamiltonien dans un $n$-cube permettait d'engendrer directement +des fonctions avec une telle caractéristique~\cite{chgw+14:oip}. +De plus, je me suis attaché à montrer l'importance +de l'équilibrage du chemin hamiltonien à enlever. + + +Les qualités statistiques des générateurs produits +ont été évalués avec succès +~\cite{bcgw11:ip,chgw+14:onp,chgw+14:oip} en se confrontant à +des batteries de tests telles que Die-Hard, NIST, TestU01. + +Plus récemment, nous avons entrepris de trouver des bornes du temps d'arrêt +d'obtention d'une distribution uniforme d'un générateur +construit en enlevant un chemin hamiltonien équilibré dans un $n$-cube. Le travail +en collaboration avec Pr. P.-C. Heam du DISC +est en cours de soumission +dans un journal international. + +Enfin j'ai été sollicité pour encadrer une thèse sur l'implantation +de générateurs de nombre pseudo-aléatoires à bases d'itérations +chaotiques sur des circuits logiques +programmables. J'ai commencé ce travail en encadrant une étude exhaustive +de toutes les instances d'implantations de cette classe. +Ce travail complet théorique et pratique est terminé aujourd'hui et +est en cours de soumission dans un journal international. + + + + + + +\subsection{Masquage d'information}\label{sub:ih} + +La propriété de transitivité des fonctions chaotiques implique que l'on peut +atteindre tout point depuis le voisinage de n'importe quel point. +Lorsqu'on cherche à embarquer une marque dans un média, +si l'on souhaite de plus que celle-ci soit robuste, \textit{i.e.}, +ne puisse pas être enlevée facilement, il paraît naturel d'embarquer +cette marque sur une grande partie du média. +L'utilisation de fonctions chaotiques +paraît alors judicieuse. + +J'ai participé à la formalisation de la méthode de +marquage de médias~\cite{bcg11b:ip,bcg11:ij} et particularisé +ceci à des images numériques fournissant un +nouveau contexte pour l'étude théorique et mathématique d'algorithmes de marquage. +La chaos-sécurité a été introduite comme une nouvelle propriété +de tels algorithmes de marquage. +Nous avons de plus montré la robustesse d'un tel marquage dans les +domaines fréquentiels usuels (DWT ou DCT). + +Des instances de ces algorithmes ont été présentées en sélectionnant de manière +pertinente les fonctions à itérer soit pour garantir une robustesse +élevée~\cite{bcfg12b:ip,bcfg+13:ip} soit pour masquer l'information dans le média +et être le moins détectable possible~\cite{bcfg12a:ip}. + +D'autre méthodes de watermarking ont été investies, +particulièrement celles basées sur la Quantization Index Modulation (QIM), méthodes +étant supposées comme les plus robustes. Mes principales contributions +sur ce travail --en collaboration avec Dr R. Darazy de l'Université Antonine au Liban +et en co-encadrant le stage de M2 de Ahmad Bittar--, +ont été +d'intégrer ceci à du marquage de document PDF puis de +présenter ce problème comme un problème d'optimisation. +Grâce à une telle présentation nous avons pu trouver les paramètre optimaux +des méthodes QIM assurant à la fois robustesse et indétectabilité. +Le travail est en cours de soumission dans un journal international. + +Lorsque l'objectif visé est l'indétectabilité, on parle de \emph{stéganographie}. +Ce domaine a été adressé en critiquant notamment les scénarios usuels d'évaluation +des algorithmes de stéganographie. J'ai proposé un cadre complémentaire permettant +d'évaluer ces schémas de masquage~\cite{fccg15:ip}. +Ceci se réalise en co-encadrant le doctorat de Y. Fadil. + +J'ai de plus participé à l'élaboration de l'algorithme STABYLO~\cite{ccg15:ij} +qui est un schéma de +stéganographie basé sur l'enfouissement de l'information dans les contours +présents dans une image. +Ce travail est en collaboration avec Pr. R. Couturier. +Mes contributions ont principalement été la formalisation de l'algorithme et +son étude de complexité. Grâce a l'optimisation de cette dernière, +nous avons pu montrer +que cet algorithme présente un excellent compromis entre sécurité +fournie et complexité. + +\subsection{Les fonctions de hachage}\label{sub:hash} +Une fonction qui calcule une empreinte servant à identifier rapidement toute +donnée fournie en entrée est une fonction de hachage. On utilise ce genre +de fonctions dès qu'on veut comparer des éléments de grande taille car il +suffit de comparer leurs empreintes (généralement de taille plus réduite). +Une telle fonction doit induire de grandes variations dans l'empreinte +lorsque l'entrée varie même très peu. C'est l'effet avalanche. Cette +condition fait penser à la forte sensibilité aux conditions initiales +d'une fonction chaotique. + +Forts de nos compétences sur les fonctions dont les itérations sont +chaotiques, nous avons proposé de nouvelles fonctions de hachage. +Celles-ci combinent des outils classiques utilisés dans les +fonctions de hachage +usuelles et des itérations de systèmes dynamiques discrets étudiés +au préalable. +Nous avons prouvé que ces fonctions sont résistantes à la +seconde pré-image. Leur complexité, polynomiale en la taille +du message et la taille de l'empreinte, a été évaluée et correspond +à ce que l'on attend d'une telle fonction. +Nous avons de plus vérifié statistiquement le critère d'avalanche. +Ces résultats ont été valorisés dans les publications~\cite{bcg11:ip,bcg12:ij}. + + + + +\subsection{Application à la génomique}\label{sub:gen} + +Ayant acquis des compétences sur certaines structures de mathématiques +discrètes (particulièrement théorie des graphes, +relations d'équivalence,\ldots), j'ai pu contribuer en bio-informatique +en les réappliquant notamment. + +Une de mes premières pistes de travail a été de proposer une méthode automatique +de construction d'un ensemble de gènes communs (nommés core-génome) +à une famille de génomes. +La méthode s'appuie sur la construction du graphe de similarité +entre les gènes quotienté selon une relation d'équivalence pour en +réduire sa taille. Chaque gène est assimilé à son représentant de +classe dans chaque génome. Le core-génome se déduit comme l'intersection +de tous les génomes. Ceci a donné lieu aux +publications~\cite{acgs13:onp,akgcs+14:oip,acgm+14:ij}. + +L'approche précédente souffrait de n'engendrer que des core-génomes de (trop) +petits cardinaux. J'ai contribué notamment +à l'amélioration de la méthode en proposant une étape d'optimisation issue +d'une adaptation discrète la méthode d'essaims particulaires~\cite{aagp+15:ip}. + +Tous ces travaux ont été réalisés en collaboration avec M. Salomon et en co-encadrant +le doctorat de B. Alkindy. + + \newpage -\section{Insertion dans l'équipe de recherche (3 pages maximum).} -Rôle personnel joué dans l'animation de la recherche au -sein de cette (ces) équipe(s), sa gestion administrative et financière. Obtention et -gestion de contrats de recherche. Collaborations internationales et insertion dans un -réseau international. Organisation de manifestations scientifiques (colloques, -congrès, diffusion des résultats de la recherche en direction du public…) ; +\section{Perspectives de recherche} + + + + +\subsection{Les codes de Gray} +L'utilisation des codes de Gray dans une démarche d'apprentissage +(d'écoulement d'air ou de fonctions chaotiques) ne s'est pas révélée comme +concluante. Dans chacun des cas, la distance de Hamming entre deux +configurations voisines peut être très petite tandis que le chemin (dans le +cycle hamitlonien) qui les relie peut être long et ce même +pour des codes équilibrés. +Je propose de travailler sur ce problème discret en mesurant la qualité +du code de Gray à l'aide d'une fonction basée sur la longueur des chemins +(du cycle hamiltonien) entre les configurations voisines. +Je pense ainsi réduire ce problème à un problème d'optimisation et dégager +une démarche de génération, comme je l'ai fait en bio-informatique. + +Jusqu'à présent, la production de codes de Gray équilibrés pour la génération +de nombres pseudo-aléatoires bute sur des problèmes d'explosion combinatoire: +les seuls algorithmes connus répondant à ce problème nécessitent a priori +plus de $10^{36}$ évaluations pour $n=8$. +Il n'est ainsi pas raisonnable de mettre en +pratique ce genre d'approche lorsque chacune de ces évaluations prend 1s. +On peut peut-être +se contenter de codes ``presque'' équilibrés , à défaut de pouvoir +trouver ceux qui seront équilibrés. +Je propose d'investiguer +dans cette thématique en exploitant des approches itératives permettant +d'obtenir des optimums locaux et trouver ainsi des codes presque équilibrés. + + + +\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, améliorer la +connaissance à ce sujet. +Les propriété établies notamment sur les temps d'arrêt devraient être conservées. +Il restera à le prouver. + + +Jusqu'à présent, une seule expérimentation d'implantation de nos générateurs +sur des dispositifs physiques comme les FPGAs a été réalisée. Celle-ci +s'est faite automatiquement à l'aide de l'outil Matlab. Si le code engendré +sur le circuit est bien une implantation fidèle à la spécification, +il n'en est pas pour autant efficace: le nombre de bits générés par surface +est plutôt faible. Nous allons exploiter les meilleures démarches mises en +exergue lors de la rédaction d'un état de l'art exhaustif sur les PRNGs +implantés sur FPGA pour produire du code optimisé. +Je prévois de réaliser ceci dans la thèse de M. Bakiri, en cours. + +Pour générer une fonction dont la matrice de Markov est doublement +stochastique, nous avons proposé principalement deux méthodes +(génération puis test, suppression de chemin hamiltonien dans un $n$-cube). +Ces deux méthodes ne passent pas à l'échelle, même pour des $n$ de petite taille. +Je pense attaquer ce problème algébriquement et en programmation logique avec +contraintes. Dans le premier cas, on peut remarquer qu'un matrice +composée de $1$ uniquement +en $(i,i+1)$ est une réponse triviale au problème. Je pense continuer l'étude +de ce genre de matrices et proposer une méthode plus générale de génération. +Je prévois de réaliser ce travail avec M. S. Contassot, Pr. à l'Université de Lorraine. +Le département DISC et l'équipe VESONTIO +a de fortes compétences en programmation logique avec +contraintes. J'ai déjà démontré que ce problème peut être soluble par cette +approche, sans avoir pour autant réussi à le faire. +Je prévois des collaborations avec l'équipe VESONTIO du DISC sur ce sujet. + + +Enfin, marcher dans une partie d'un $n$-cube est le modèle théorique que +nous avons établi pour notre classe de générateurs. On pourrait cependant +penser à ``sauter'' dans ce $n$-cube, c'est à dire modifier plusieurs bits +en une seule itération. J'ai commencé à étudier ce modèle avec les résultats +pratiques suivants: le nombre d'itérations suffisant pour un mélange +correct est plus petit que celui obtenu en marchant. De plus, +il diminue à mesure que $n$ augmente ce qui n'est pas le cas en marchant. +Pour l'instant, nous n'avons pas réussi à obtenir des bornes +du temps d'arrêt. Je propose d'investiguer aussi dans cette direction. + + + +\subsection{Masquage d'information} + +Concernant le marquage de données, plusieurs approches duales cohabitent pour +établir ou non la sécurité d'un algorithme +de cette classe: les probabilistes (stego-securité par ex.), +les métriques (chaos-securité par ex.), +les cryptographiques (mesure de fuite d'information). +Notre approche n'a pas encore été évaluée selon cette dernière métrique, ce +que je propose de faire. + +Concernant l'indétectabilité, je propose de travailler à la fois sur +la stéganographie et sur la stéganalyse. +Nos expériences sur les schémas les plus efficaces de stéganographie +nous font penser qu'embarquer un message dans les contours comme cela l'a été fait pour +STABYLO est perfectible: on sait depuis qu'il existe des fonctions mathématiques +qui modélisent ces contours. Lorsqu'on modifie sans garde la valeur des bits de ces +contours, la ``continuité'' des fonctions qui les modélisent peut être perdue et +le message peut s'en trouver détectable. Que je sache, aucune approche de stéganographie +basée sur la continuité des fonctions de contours n'a jamais été proposée. +Je propose donc d'investiguer dans cette voie. + +Les démarches de stéganalyse sont souvent composées de 2 étapes: +caractérisation puis classification. +On extrait au préalable une grande quantité des caractéristiques du média +puis on utilise une méthode de +classification basée sur celles-ci. La communauté voit souvent cette +seconde étape comme une boite noire et se concentre +sur la construction de l'ensemble des caractéristiques les plus discriminantes. +Autant que je sache, les méthodes algébriques +de réduction de domaine (analyse par composant principaux, SVD) +ont rarement été utilisées comme une étape intermédiaire entre la caractérisation et +la classification. Ces méthodes ont déjà été +appliquées avec succès lorsqu'elles sont combinées avec des méthodes +d'apprentissage, par exemple dans de la reconnaissance faciale. +Je propose d'étudier cette piste dans ce domaine. +Ceci se réalisera notamment au travers du doctorat de Y. Fadil. + + + + + \newpage -\section{Encadrement et co-encadrement d'étudiants (1 page)} (maîtrise, DEA, thèses d'Université, -stages d'ingénieurs…) pour des activités de recherche en indiquant de manière -explicite la part d’encadrement assurée par le candidat à l’HDR ; +\section{Insertion dans l'équipe de recherche} + +La thématique principale de ma thèse et du post-doctorat qui a suivi +était la vérification de programmes par preuve automatique, soit de +la logique informatique. +Suite à mon recrutement dans l'équipe AND, mes recherches se sont réorientées +autour des SDDs et donc de l'analyse numérique plus généralement. +En plus des publications obtenues avec les membres de l'équipe AND, +ce qui suit récapitule quelques éléments permettant +d'apprécier mon insertion dans l'équipe AND + + + + +J'ai monté une collaboration active avec l'Université Antonine au Liban. +J'y ai été invité en mai 2013. J'ai par la suite co-encadré trois stages de +Master 2 recherche avec des membres de cette université. +J'ai un article en cours de soumission résumant un travail en collaboration +avec un ancien étudiant et un enseignant chercheur de cette université. + +Je suis membre du GDR codes et cryptographie. J'ai à ce titre +participé aux Journées Codes et Stéganographie en 2012 (Rennes) +où j'ai présenté le travail +de \og Steganography: secure and robust algorithms \fg{} et en 2013 (Paris). + + +J'ai co-organisé avec J. Bahi et C. Guyeux +\og The First Workshop on Information Hiding Techniques +for Internet Anonymity and Privacy (IHTIAP) \fg{} à Venise en juin 2012. +Le comité de programme était composé +de 18 chercheurs internationaux (dont je faisais aussi partie). +Il s'est déroulé sur 1 journée. + + +J'ai fait partie des comités de programme de conférences +comme \og international conference on evolving internet \fg{} +(2012, 2013,2014 )\ldots +J'ai été session chair de \og international conference on evolving internet\fg{} +en 2011 et IHTIAP en 2012 + +J'ai reviewé des articles pour les journaux internationaux +suivants: The computer Journal, Springer Multimedia Tool and application, +Springer Annals in Telecommunication\ldots + + +Je suis régulièrement membre de jury des épreuves TIPE, épreuves communes +à 90 concours d'ingénieurs (sessions 2012 et 2015) et fournis +à chaque session des sujets scientifiques pour l'épreuve. + + \newpage -\section{Participation éventuelle à des tâches administratives d'intérêt collectif (1 à 2 pages)}, -à l'activité d'enseignement, ou expérience en entreprise ; +\section{Encadrement et co-encadrement d'étudiants} + +\subsection{Thèse d'université} + +Je co-encadre (à hauteur de 40\%) avec Michel Salomon (40\%) et +Jacques M. Bahi (20\%) le doctorat de Bassam Alkindy +sur les combinaisons d'approches pour la prédiction de l'évolution génomique. +Le doctorat a commencé en septembre 2012 et devrait être soutenu en +novembre 2015. +Ce travail de thèse a donné lieu à 6 publications dans des conférences +internationales. + + +Je co-encadre (à hauteur de 50\%) avec Christophe Guyeux (50\%) +le doctorat de Youssra Fadil +sur +l'étude du comportement des outils d'intelligence artificielle +face à des dynamiques complexes. +Le doctorat a commencé en décembre 2013 et devrait être soutenu en +décembre 2016. +Ce travail de thèse a donné lieu à 1 publication dans une conférence +internationale. + + +Je co-encadre (à hauteur de 50\%) avec Christophe Guyeux (50\%) +le doctorat de Mohamed Bakiri +sur +l'implémentation matérielle de générateurs de nombres pseudo-aléatoires basés sur les itérations chaotiques. +Le doctorat a commencé en septembre 2014 et devrait être soutenu en +aout 2017. +Ce travail de thèse a donné lieu à 1 publication dans un journal international +en cours de soumission. + +\subsection{Master 2 recherche} + + +J'ai co-encadré (à hauteur de 34\%) avec Raphael Couturier (33\%) et +Rony Darazi -- Université Antonine au Liban--(33\%) +le stage de recherche de Master 2 de Ahmad Bittar +sur +la +Steganography in PDF documents based on Unprintable Control ASCII Codes. +Le stage a commencé le 01 mai 2013 et a été soutenu le 30 septembre 2013. +Ce travail de Master a donné lieu à 1 publication dans un journal international +en cours de soumission (en révision mineure). + + + + +J'ai co-encadré (à hauteur de 80\%) avec +Talar Atechian -- Université Antonine au Liban--(20\%) +le stage de recherche de Master 2 de Hussein Nasser +sur +une +Critical Analysis of Distributed Algorithm for Sensor +Network Lifetime Maximization. +Le stage a commencé le 01 avril 2014 et a été soutenu le 31 août 2014. + + +Je co-encadre (à hauteur de 80\%) avec +Talar Atechian -- Université Antonine au Liban--(20\%) +le stage de recherche de Master 2 de Khaled Daher +sur la désynchronisation du calcul d'optimisation de la durée de vie +d'un réseau de capteurs. +Le stage a commencé le 01 avril 2015 et sera soutenu le 31 août 2015. + \newpage -\section{Liste des publications} -selon le plan suivant : Internationales avec comité de -lecture ; Nationales avec comité de lecture ; Didactiques et non référencées ; -Chapitres de livres et documents multi-médias ; Compte-rendu de colloques (avec -sélection sur résumés puis sans sélection sur résumés) ; +\section{Participation à des tâches d'intérêt collectif} + +Depuis septembre 2000, je suis titulaire à l'Université de Franche-Comté, +soit sur un poste de PrCe (de 2000 à 2008, sauf l'année 2006-2007) soit sur +un poste de MdC. J'ai assuré un grand nombre d'enseignements de la première +année de licence ou de DUT jusqu'en seconde année de Master. Depuis mon +recrutement comme MdC, j'ai recentré mes enseignements autour +de mes thématiques de recherche, à savoir essentiellement les +mathématiques discrètes. +Je suis de plus le coordinateur des enseignements de mathématiques +au département d'informatique de l'IUT BM. + +J'ai été membre élu du conseil d'institut de l'IUT BM +de 2011 à 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. + +Depuis septembre 2014, je suis le responsable du parcours TeProw +de la Licence Pro Conception des Application Multi-tiers 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. + + + + \newpage -\section{Liste des communications} - selon le plan suivant : Conférences sur invitation -personnelle ; Communication à des colloques, avec sélection sur résumés ; -Internationaux ; Nationaux ; Communications diverses. -\bibliographystyle{alpha} -\bibliography{biblio} -\include{Bibliographie} +\section{Publications après la thèse} + +\subsection{Journaux internationaux avec comité de sélection} + +\begin{thebibliography}{CHG{\etalchar{+}}14b} + +\bibitem[CCG15]{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]{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[BCG12a]{bcg12:ij} +Jacques Bahi, Jean-Fran\c{c}ois Couchot, and Christophe Guyeux. +\newblock Quality analysis of a chaotic proven keyed hash function. +\newblock {\em International Journal On Advances in Internet Technology}, + 5(1):26--33, 2012. + +\bibitem[BCG12b]{bcg11:ij} +Jacques Bahi, Jean-Fran\c{c}ois Couchot, and Christophe Guyeux. +\newblock Steganography: a class of secure and robust algorithms. +\newblock {\em The Computer Journal}, 55(6):653--666, 2012. + +\bibitem[BCGS12]{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. + +\end{thebibliography} + +\subsection{Conférences internationales avec comité de sélection} + +\begin{thebibliography}{CHG{\etalchar{+}}14b} + +\bibitem[AAG{\etalchar{+}}15]{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[ACG{\etalchar{+}}14]{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[ACGS13]{acgs13:onp} +Bassam Alkindy, Jean-Fran\c{c}ois Couchot, Christophe Guyeux, and Michel + Salomon. +\newblock Finding the core-genes of chloroplast species. +\newblock Journ\'ees SeqBio 2013, Montpellier, November 2013. + +\bibitem[AGC{\etalchar{+}}14]{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[BCDG07]{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[BCF{\etalchar{+}}13]{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[BCFG12a]{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]{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[BCG11a]{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]{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]{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]{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[BCVC10]{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[CD07]{CouchotD07IFM} +Jean-Fran\c{c}ois Couchot and Fr\'ed\'eric Dadeau. +\newblock Guiding the correction of parameterized specifications. +\newblock In {\em IFM'07, 6th Int. Conf. on Integrated Formal Methods}, volume + 4591 of {\em LNCS}, pages 176--194, Oxford, UK, July 2007. Springer. + + +\bibitem[CDS12]{cds12:ip} +Jean-Fran\c{c}ois Couchot, Karine Deschinkel, and Michel Salomon. +\newblock Suitability of artificial neural network for {MEMS}-based flow + control. +\newblock In Julien Bourgeois and Michel de~Labachelerie, editors, {\em dMEMS + 2012, Workshop on design, control and software implementation for distributed + MEMS}, pages 1--6, Besan\c{c}on, France, April 2012. IEEE CPS. + +\bibitem[CGS09]{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[CH07]{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[CHG{\etalchar{+}}14a]{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[CL07]{couchot07cade} +Jean-Fran\c{c}ois Couchot and S.~Lescuyer. +\newblock Handling polymorphism in automated deduction. +\newblock In {\em CADE'07, 21st Int. Conf. on Automated Deduction}, volume 4603 + of {\em LNCS}, pages 263--278, Bremen, Germany, July 2007. Springer. + +\bibitem[Cou10]{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[FCCG15]{fccg15:ip} +Yousra~Ahmed Fadil, Jean-Fran\c{c}ois Couchot, Rapha\"el Couturier, and + Christophe Guyeux. +\newblock Steganalyzer performances in operational contexts. +\newblock In {\em IIH-MSP 2015, 11th Int. Conf. on Intelligent Information + Hiding and Multimedia Signal Processing}, pages ***--***, Adelaide, + Australia, September 2015. +\newblock To appear. + +\end{thebibliography} + +\subsection{Communications orales invitées} + +J'ai été invité: +\begin{itemize} + +\item au Workshop \og Théorie des réseaux booléens et ses applications en biologie\fg{} +à Nice en novembre 2014; + +\item à la journée \og Advances in Mobile Technologies Day\fg{} par l'Université Antonine (Liban) en mai 2013; + +\item au Séminaire MDSC (Modèles Discrets pour les Systèmes Complexes) + du laboratoire I3S sur le sujet \og Efficiently dealing with SMT-LIB provers in software verification\fg{} en décembre 2007. +\end{itemize} + +\subsection{Communications diverses} +\begin{thebibliography}{CHG{\etalchar{+}}14b} + +\bibitem[CHG{\etalchar{+}}14b]{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{alpha} +%\bibliography{abbrev,biblioand} + \end{document}