]> AND Private Git Repository - hdrcouchot.git/blobdiff - demandeInscription/synthese.tex
Logo AND Algorithmique Numérique Distribuée

Private GIT Repository
synthèse masquage
[hdrcouchot.git] / demandeInscription / synthese.tex
index a9ba499aa0e113f9a46ba0c54566272b56466996..38b34974aa5347351636684d94eb5e0e476bc518 100755 (executable)
@@ -58,9 +58,9 @@
      %bookmarks=true, %créé des signets pour Acrobat
      bookmarksopen=true,            %si les signets Acrobat sont créés,
                                     %les afficher complÚtement.
      %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.
 }
 
 
 }
 
 
@@ -140,28 +140,405 @@ mention très honorable.
  \end{itemize}
 
 
  \end{itemize}
 
 
-\section{Nom et type de l'équipe de recherche (1 page).}
+\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.
 
 
 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 son
-annexés à cette synthèse.
-\JFC{joindre l'avis de Raphale, d'Olga de Nicolas et de PH. Lutz} 
+L'avis du directeur de l'équipe et du directeur de l'école doctorale es
+annexé à cette synthèse (section~\ref{sec:avis:directeur}).
+\JFC{joindre l'avis de Raphaël, d'Olga de Nicolas et de PH. Lutz} 
 
 
 \newpage
 
 
 \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 ;
+\section{Résumé de la thématique de la thèse d'université (1 page)}
+On considère en entrée de la démarche une description
+mathématique d'un programme: par exemple une fonction enrichie avec  
+une  spécification du contexte dans lequel elle est invoquée (la pré-condition) et 
+une spécification exprimant quelles  propriétés sont garanties en retour (la
+post-condition). Lorsque pré-condition et post-condition sont équivalentes,
+on parle d'invariant.
+La thématique de \emph{vérification de programmes par preuve automatique} 
+consiste à tout d'abord construire des formules mathématiques 
+qui doivent être vraies si et seulement si 
+la post-condition est établie par le programme sous hypothèse de pré-condition,
+puis ensuite à 
+décharger ces formules dans des prouveurs de théorèmes. 
+Cette thématique est au c{\oe}ur des travaux de recherche effectués
+pendant mon doctorat et le post-doctorat qui a suivi à à l'Inria.
+
+
+
+Durant mon travail de thèse intitulée 
+{\em vérification d'invariants par superposition}, 
+j'ai proposé différentes traductions en logique équationnelle 
+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. 
+
+Lors de mon postdoc à l'INRIA, j'ai d'abord montré qu'il était possible
+d'instancier des contre-exemple~\cite{BCDG07} et de voir 
+si ceux-ci sont atteignables~\cite{CouchotD07IFM} lorsque 
+l'obligation de preuve à vérifier n'est pas établie.
+Ceci peut aider l'ingénieur à corriger ses modèles.
+Je  me suis ensuite intéressé  à la
+logique du premier ordre polymorphe. 
+Dans ce but, j'ai présenté un réducteur de logique
+polymorphe vers de la logique sans sorte et de la logique multi-sorte
+du premier ordre, préservant la correction et la
+complétude~\cite{couchot07cade}. 
+Toujours pendant mon post-doctorat, face au problème d'explosion
+combinatoire rencontré  
+lors de déduction automatique, j'ai présenté une approche
+de réduction de
+formules~\cite{couchot07FTP, cgs09:ip} de type SMT-LIB
+basée sur la sélection des hypothèses les plus  
+pertinentes.   
+L'approche a été implantée et validée sur un exemple industriel réel
+de 5000 lignes de Code C annoté fourni par Dassault aviation.
+
+
+
+
+
+
+
+\subsection*{Publications issues de ces recherches}
+\begin{enumerate}
+
+\item \label{cgs09:ip}[CGS09],
+J.-F. Couchot and A. Giorgetti  and N. Stouls, 
+{G}raph {B}ased {R}eduction of {P}rogram {V}erification {C}onditions.
+In AFM'09, {A}utomated {F}ormal {M}ethods (colocated with {CAV}'09),
+pages 40--47, Grenoble, 2009, {ACM Press}. 
+
+
+\item\label{couchot07cade}[CL07]
+J.-F. Couchot and S. Lescuyer.
+Handling polymorphism in automated deduction.
+In {\em 21th International Conference on Automated Deduction
+  (CADE-21)}, volume 4603 of {\em LNCS (LNAI)}, pages 263--278, Bremen,
+  Germany, July 2007.
+
+\item\label{CouchotD07IFM}[CD07]
+J.-F. Couchot and F. Dadeau.
+Guiding the correction of parameterized specifications.
+In {\em Integrated Formal Methods}, volume 4591 of {\em Lecture Notes
+  in Computer Science}, pages 176--194, Oxford, UK, July
+2007. Springer.
+
+\item\label{CH07}[CH07]
+J.-F. Couchot and T. Hubert.
+A Graph-based Strategy for the Selection of Hypotheses.
+In {\em FTP 2007 - International Workshop on First-Order Theorem
+  Proving}, pages 63--76, Liverpool, UK, September 2007.
+
+
+\item \label{BCDG07}[BCDG07]
+F.~Bouquet, J.-F. Couchot, F.~Dadeau, and A.~Giorgetti.
+Instantiation of parameterized data structures for model-based
+  testing.
+In {\em B'2007, the 7th Int. B Conference}, volume 4355 of {\em
+  LNCS}, pages 96--110, Besancon, France, January 2007, Springer.  
+
+
+
+\item\label{CGK05}[CGK05]
+J.-F. Couchot, A.~Giorgetti, and N.~Kosmatov.
+ A uniform deductive approach for parameterized protocol safety.
+ {\em ASE '05: Proceedings of the 20th IEEE International
+  Conference on Automated Software Engineering}. 
+IEEE Computer Society, pages 364--367, novembre 2005.
+
+
+
+\item\label{CDDGR03}[CDD$^{+}$03]
+J.-F. Couchot, F.~Dadeau, D.~D\'{e}harbe, A.~Giorgetti, and S.~Ranise.
+Proving and debugging set-based specifications.
+{\em Electronic Notes in Theoretical Computer Science, proceedings
+  of the Sixth Brazilian Workshop on Formal Methods (WMF'03)}, volume~95, pages
+  189--208, mai 2004.
+
+\item\label{CDGR03}[CDGR03] %(\textbf{part}~: 25\%)
+J.-F. Couchot, D.~D\'{e}harbe, A.~Giorgetti, and S.~Ranise.
+Scalable automated proving and debugging of set-based specifications.
+{\em Journal of the Brazilian Computer Society}, 9(2):17--36,
+  novembre 2003).
+
+
+
+\item\label{CG04}[CG04]
+J.-F. Couchot and A.~Giorgetti.
+Analyse d'atteignabilit\'e d\'eductive.
+{\em Congr\`es Approches Formelles dans
+  l'Assistance au D\'eveloppement de Logiciels (AFADL'04)},  pages 269--283,
+  juin 2004.
+%VERIFIE
+
+\end{enumerate}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 
 \newpage
 
 \newpage
-\section{Exposé des recherches réalisées au cours de la période postdoctorale (5 pages maximum)}
+\section{Exposé des recherches réalisées au cours de la période postdoctorale}
+\JFC{chapeau à refaire}
+
+
+\subsection{Convergence de systèmes  dynamiques discrets}
+
+Un système dynamique discret (SDD) est une fonction $f$ 
+du $n$-cube ($\{0,1\}^n$) dans lui même et un mode opératoire
+(parallèle, unaire, généralisé) qui peut être itéré 
+en synchrone ou en asynchrone.
+Ils ont été étudiés à de maintes reprises~\cite{Rob95,Bah00,bcv02}.
+Pour chacun de ces modes, il existe des critères  (suffisants) de convergence
+globale ou locale, souvent basés sur le fait que  $f$ est  
+est un opérateur contractant ans un espace.
+
+Les modes  asynchrones ont une dynamique avec plus de liberté 
+puisqu'ils autorisent chaque élément à modifier sa valeur avant 
+de connaître les valeurs des autres éléments dont il dépend. 
+Cependant, lorsque les calculs à effectuer sur certains n{\oe}uds
+sont coûteux en temps et/ou que les temps de communication sont élevés,   
+ces modes peuvent présenter une convergence plus rapide que le cas synchrone.  
+
+Dans~\cite{BCVC10:ir}, j'ai formalisé le mode des 
+\emph{itérations mixes} (introduit dans~\cite{abcvs05})
+qui combine synchronisme et asynchronisme.
+Intuitivement, les n{\oe}uds qui pourraient engendrer des cycles dans 
+les itérations asynchrones sont regroupés dans une même classe. 
+Les noeuds à l'intérieur celle-ci groupe seront itérés de manière 
+synchrone et les itérations asynchrones sont conservées entre les groupes. 
+Pour gommer les  différences entre les n{\oe}uds d'une même classe
+lorsqu'ils  sont vus depuis des n{\oe}uds extérieurs, j'ai défini le 
+mode des \emph{itérations mixes avec délais uniformes}.
+
+
+Grâce à cette formalisation, j'ai pu énoncer puis démontrer un théorème 
+établissant que pour des conditions classiques de convergence des itérations
+synchrones d'une fonction $f$, les itérations mixes à délai uniforme
+convergent aussi vers le même point fixe.
+
+
+L'étude de convergence de SDD est simple à vérifier 
+pratiquement pour le mode synchrone. Lorsqu'on introduit des stratégies 
+pseudo périodiques pour les modes unaires et généralisées, le problème 
+se complexifie. C'est pire encore lorsqu'on traite des itérations asynchrones 
+et mixes prenant de plus en compte les délais. 
+Des méthodes de simulation basées sur des stratégies et des délais générés aléatoirement ont déjà été présentées~\cite{BM99,bcv02}.
+Cependant, comme ces implantations ne sont pas exhaustives, elles ne sont intéressantes que lorsqu'elles fournissent un contre-exemple. 
+Lorsqu'elles exhibent une convergence,  
+cela ne permet que donner une intuition de convergence, pas  une preuve.
+Autant que je sache, aucune démarche de preuve formelle automatique 
+de convergence n'avait jamais été établie. 
+
+
+J'ai montré dans~\cite{Cou10:ir} comment  simuler 
+des SDDs selon tous les modes pour établir 
+formellement leur convergence (ou pas).
+Cette simulation est basée sur l'outil SPIN de \emph{Model-Checking}
+qui est une classe d'outils adressant le problème de vérifier automatiquement
+qu'un modèle vérifie une propriété donnée. Pour traiter le problème d'explosion 
+combinatoire, les outils de cette classe 
+appliquent des méthodes d'ordre partiel, d'abstraction,
+de quotientage selon une relation d'équivalence.
+
+Pour cela, j'ai présenté pour cela une démarche de traduction d'un SDD  
+dans PROMELA qui est le langage de SPIN.
+J'ai énoncé puis prouvé ensuite la  correction et la complétude de la démarche
+Des données pratiques comme la complexité et des synthèses d'expérimentation
+ont aussi été fournies.
+
+
+
+\subsection{Construction de fonctions chaotiques}
+Pr. Christophe Guyeux de l'équipe AND a proposé dans sa thèse~\cite{guyeuxphd} 
+une caractérisation des fonctions $f$ de $\{0,1\}^n$ dans lui même 
+dont les itérations sont chaotiques selon Devanney dans certains mode: 
+il est nécessaire et suffisant que son graphe des itérations soit
+fortement connexe.  
+J'ai proposé plusieurs méthodes de construction de 
+fonctions ayant de tels graphes d'itérations~\cite{bcgr11:ip,chgw+14:onp}.
+
+Dans la première~\cite{bcgr11:ip},
+l'algorithme enlève des arcs et vérifie ensuite que  
+la forte connexité est maintenue.
+Même si cet algorithme retourne toujours des fonctions dont le graphe 
+des itérations est fortement connexe, il n'en est pas pour autant efficace 
+car il  nécessite une vérification à posteriori de la 
+forte connexité sur le graphe entier composé de  $2^n$ sommets.
+La seconde méthode propose une solution à ce problème en présentant
+des conditions suffisantes sur un graphe à $n$ sommets
+qui permettent d'obtenir des graphes d'itérations fortement connexes.
+Ce théorème a aussi été prouvé dans~\cite{bcgr11:ip}
+et des instanciations effectives 
+ont été produites. 
+Une troisième méthode~\cite{chgw+14:onp} s'appuie sur les codes 
+de Gray, ou de manière équivalente sur les cycles hamiltoniens du graphe des
+itérations: un cycle qui visite chaque n{\oe}ud exactement une fois est un  
+\emph{cycle hamiltonien}.
+La démarche consiste à enlever du graphe un de ses cycles hamiltoniens dont 
+la démarche de génération est un problème connu. 
+
+Ces méthodes ont permis d'étendre à l'infini la classe des fonctions 
+dont les itérations sont chaotiques.
+
+
+\subsection{Apprentissage par réseaux neuronaux}
+Nous disposons grâce aux travaux présentés à la section précédente d'un grand
+nombre de fonctions dont les itérations sont chaotiques.
+Nous avons entrepris d'étudier ces itérations et plus particulièrement leur 
+apprentissage par un réseau de neurones. 
+J'ai notamment pu contribuer à montrer pratiquement qu'il
+est très difficile (voir impossible) de les prédire 
+à l'aide de tels outils d'intelligence artificielle~\cite{bcgs12:ij}.
+
+
+Nous nous sommes attaqués à un problème physique d'optimisation de  
+l'écoulement d'un flux d'air le long d'un véhicule. 
+Ce flux peut être modifié si l'on active des injecteurs d'air placés 
+par exemple sur le becquet du véhicule. 
+Le flux d'air peut être modélisé à l'aide d'équations de Navier-Stokes
+dont on ne connaît pas de méthode analytique de résolution. 
+De plus, le nombre de Reynolds calculé dans cette situation fait apparaître 
+que le régime est extrêmement turbulent, donc difficile à prévoir.
+Nous avons souhaité 
+continuer nos expériences d'apprentissage à l'aide 
+de réseau de neurones dans ce contexte~\cite{cds12:ip,cds13:ij}.
+Il est apparu comme judicieux de mémoriser les configurations
+représentant l'état des actionneurs à l'aide de nombres binaires.
+De plus les codes de Gray, dont deux mots adjacents ne diffèrent que d'un 
+bit se sont présentés comme une des manière de mémoriser les sorties du 
+réseau de neuronnes comme un seul nombre binaire.
+Quand on sait que trouver un chemin hamiltonien (comme étudié dans la partie précédente) dans un
+$n$-cube revient à trouver un code 
+de Gray dans un mot de $n$-bits. Les compétences acquises lors du travail 
+sur les chemins hamiltoniens ont ainsi pu être réutilisées et approfondies.
+Les résultats pratiques quant à l'utilisation de ces codes ce sont cependant 
+révélés comme moins pertinents que l'utilisation de $n$ sorties.
+
+\subsection{Génération de nombres pseudo-aléatoires}
+
+Au commencement de ce travail, notre équipe disposait d'un générateur de nombres 
+pseudo-aléatoires (PRNG) 
+basé sur une seule fonction dont nous avions prouvé la chaoticité 
+des itérations, à savoir la négation booléenne vectorielle. Cependant pour 
+réussir les tests statistiques dédiées aux PRNGs, il était nécessaire d'itérer 
+un grand nombre (arbitraire) de fois cette fonction entre deux 
+sorties. 
+
+Avec la production d'une grande collection de fonctions à itérations chaotiques, 
+j'ai proposé de répondre à la question suivante: comment engendrer des fonctions 
+dont les itérations vont produire des nombres simulant correctement l'aléa.
+J'ai d'abord caractérisé les fonctions dont les itérations produisent des nombres 
+selon une distribution uniforme~\cite{bcgr11:ip}. Pour cela il a fallu réécrire
+l'algorithme de génération comme une marche aléatoire dans une partie du $n$-cube,
+de se ramener à une chaîne de Markov puis d'utiliser la théorie élaborée sur ce sujet 
+pour conclure. Par la même occasion, nous avons démontré que certaines fonctions 
+chaotiques ne peuvent pas produire un aléa suivant une distribution uniforme.
+La sortie est biaisée.
+
+J'ai proposé ensuite des méthodes permettant de trouver de telles 
+fonctions en commençant par filtrer celles qui ne disposent pas 
+de cette caractéristique parmi toutes les fonctions chaotiques qui peuvent 
+être engendrées~\cite{bcgr11:ip}. J'ai démontré ensuite que supprimer 
+un cycle hamiltonien dans un $n$-cube permettait d'engendrer directement 
+des fonctions avec une telle caractéristique~\cite{chgw+14:oip}.
+De plus, je me suis attaché à montrer l'importance 
+de l'équilibrage du chemin hamiltonien à enlever. 
+
+Les générateurs produits ont d'abord été évalués avec succès
+ont confirmé la qualité de 
+ceux-ci~\cite{bcgw11:ip,chgw+14:onp,chgw+14:oip} en se confrontant à 
+des batteries de tests telles que Die-Hard, NIST, TestU01.
+
+Plus récemment, nous avons entrepris de trouver des bornes du temps d'arrêt
+d'obtention d'une distribution uniforme d'un générateur construit en enlevant un chemin hamiltonien équilibré dans un $n$-cube. Le travail est en cours de soumission
+en journal international.
+
+
+
+\subsection{Masquage d'information}
+
+La propriété de transitivité des fonctions chaotiques implique que l'on peut 
+atteindre tout point depuis le voisinage de n'importe quel point.
+Lorsqu'on cherche à embarquer une marque dans un media, 
+si l'on souhaite de plus que celle-ci soit robuste, \textit{i.e.},
+ne puisse pas être enlevée facilement, il paraît naturel d'embarquer 
+cette marque sur une grande partie du media. L'utilisation de fonctions chaotique
+paraît alors judicieuse.
+
+J'ai participé à la formalisation de la méthode de
+marquage de médias~\cite{bcg11b:ip,bcg11:ij} et particularisé
+ceci à des images numériques fournissant un 
+nouveau contexte pour l'étude théorique et mathématique d'algorithmes de marquage.
+La chaos-sécurité a été introduite comme une nouvelle propriété 
+de tels algorithmes de marquage comme existe
+déjà la ($\epsilon$-)stego-securité.
+Nous avons de plus montré la robustesse d'un tel marquage dans les 
+domaines fréquentiels usuel (DWT et  DCT domains).
+
+Des instances de ces algorithmes ont été présentées en sélectionnant de manière 
+pertinenente les fonctions à itérer soit pour garantir une robustesse 
+élevée~\cite{bcfg12b:ip,bcfg+13:ip} soit pour masquer l'information dans le média 
+et être le moins détectable possible~\cite{bcfg12a:ip}. 
+
+D'autre méthodes de watermarking ont été investiguées 
+particulièrement celles basées sur la Quantization Index Modulation (QIM), méthodes 
+étant supposées comme les plus robustes. Mes principales contributions 
+sur ce travail --en collaboration avec des membres de l'Université Antonine au Liban--,
+ont été 
+d'intégrer ceci à du marquage de document PDF puis de 
+présenter ce problème comme un problème d'optimisation. 
+Grâce à une telle présentation nous avons pu trouver les paramètre optimaux
+des méthodes QIM assurant à la fois robustesse et indetectabilité.
+Le travail est en cours de soumission en journal international.
+
+Lorsque l'objectif visé est l'indétectabilité, on parle de \emph{stéganographie}.
+Ce domaine a été adressé en critiquant notament les scenarios usuels d'évaluation
+des algorithmes de steganographie. J'ai proposé un cadre complémentaire permettant 
+d'apprécier ces schémas de masquage~\cite{fccg15:ip}.
+J'ai deplus participé à l'élaboration de l'algorithme STABYLO~\cite{ccg15:ij}
+qui est un schéma de
+stéganographie basé l'enfouissement de l'information dans les contours 
+d'une image. Ma contribution a principalement été la formalisation de l'algorithme, 
+son étude de complexité. Grâce a l'optimisation de cette dernière,
+nous avons  pu montrer 
+que cet algorihtme présente un excellent compromis entre la  sécurité
+fournie et sa complexité.  
+
+
+
+
+
+\subsection{Application à la génomique}  
+
+Core génome 
+
+
+
+\subsection*{Publications issues de ces recherches}
 
 
-(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)}
 
 \newpage
 \section{Perspectives de recherche (1 à 2 pages maximum)}
@@ -195,9 +572,12 @@ sélection sur résumés puis sans sélection sur résumés) ;
  selon le plan suivant : Conférences sur invitation
 personnelle ; Communication à des colloques, avec sélection sur résumés ;
 Internationaux ; Nationaux ; Communications diverses.
  selon le plan suivant : Conférences sur invitation
 personnelle ; Communication à des colloques, avec sélection sur résumés ;
 Internationaux ; Nationaux ; Communications diverses.
+
+\section{Avis du directeur de l'Equipe}\label{sec:avis:directeur}
+
 \bibliographystyle{alpha}
 \bibliographystyle{alpha}
-\bibliography{biblio}
-\include{Bibliographie}
+\bibliography{abbrev,biblioand}
+
 
 
 \end{document}
 
 
 \end{document}