%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.
}
\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)}
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}
