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

Private GIT Repository
ajout d'unesynthèse
[hdrcouchot.git] / demandeInscription / synthese.tex
index a9ba499aa0e113f9a46ba0c54566272b56466996..0d467aa2ec76ed6f67b161fd6a5663fc2cdc67ab 100755 (executable)
@@ -58,8 +58,8 @@
      %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
+     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.
 }
 
      pdfsubject={Algèbre et géométrie}          %sous Acrobat.
 }
 
@@ -140,28 +140,335 @@ 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.
+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 Raphale, d'Olga de Nicolas et de PH. Lutz} 
 
 
 \newpage
 \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)}
 
 \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)}
 
 \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.
  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}