X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/ab856c6a43de1e2a3bdbc0361e1da1e4da76a3d1..54b170f26af2fb6bf6150f003918ac5992314293:/demandeInscription/synthese.tex?ds=inline

diff --git a/demandeInscription/synthese.tex b/demandeInscription/synthese.tex
index a9ba499..0d467aa 100755
--- a/demandeInscription/synthese.tex
+++ b/demandeInscription/synthese.tex
@@ -58,8 +58,8 @@
      %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
+     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={AlgÃ¨bre et gÃ©omÃ©trie}          %sous Acrobat.
 }
 
@@ -140,28 +140,335 @@ mention trÃ¨s honorable.
  \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.
 
-L'avis du directeur de l'Ã©quipe et du directeur de l'Ã©cole doctorale sont 
-annexÃ©s Ã  cette synthÃ¨se.
+L'avis du directeur de l'Ã©quipe et du directeur de l'Ã©cole doctorale est 
+annexÃ© Ã  cette synthÃ¨se (section~\ref{sec:avis:directeur}).
 \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 ;
+\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Ã©cfication 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
 \section{ExposÃ© des recherches rÃ©alisÃ©es au cours de la pÃ©riode postdoctorale (5 pages maximum)}
+\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 delais 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:oip}.
+
+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 Ã  postÃ©riori de la 
+forte connexitÃ© sur le graphe entier composÃ© de  $2^n$ sommets.
+La seconde mÃ©thode propose une solution Ã  ce problÃ¨me en prÃ©sentant
+des conditions suffisantes sur un graphe Ã  $n$ sommets
+qui permettent d'obtenir des graphes d'itÃ©rations fortement connexes.
+Ce thÃ©orÃ¨me a aussi Ã©tÃ© prouvÃ© dans~\cite{bcgr11:ip}
+et des instanciations effectives 
+ont Ã©tÃ© produites. 
+Une troisiÃ¨me mÃ©thode~\cite{chgw+14:oip} 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Ãªment 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}
+
+Plein de fonctions chaotiques : cependant chaos n'est pas alÃ©atoire et pseudo 
+alÃ©atoire. 
+
+Condition nÃ©cessaire et suffisante : matrice de Markov doublement sotchastique
+
+mÃ©thode 1 : gÃ©nÃ©ration de fonction chaotiques par thÃ©orÃ¨me FCT puis 
+filtrage de celles qui sont doublement stochastiques
+
+mÃ©thode 2 : directe par suppression de cycles hamiltonien
+
+Evaluation statistique
+
+Mesure de la qualitÃ© (stoping time)
+
+
+\subsection{Masquage d'information}
+
+Formalisation de la mÃ©thode 
+
+
+
+
+\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)}
@@ -195,9 +502,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.
+
+\section{Avis du directeur de l'Equipe}\label{sec:avis:directeur}
+
 \bibliographystyle{alpha}
-\bibliography{biblio}
-\include{Bibliographie}
+\bibliography{abbrev,biblioand}
+
 
 
 \end{document}
