[hdrcouchot.git] / demandeInscription / synthese.tex

\documentclass[a4paper,french,11pt]{article}
%\usepackage{hyperlatex}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{framed}
\usepackage[amsmath,thmmarks,thref,framed]{ntheorem}
\usepackage[dvips]{graphics}
\usepackage{epsfig}
\usepackage{epsfig,psfrag}
\usepackage{subfigure}
\usepackage{color}
\usepackage{calc}
\usepackage{url}
\usepackage{longtable}
\usepackage{tabls}
\usepackage{textcomp}
%\usepackage{slashbox}
\usepackage{gastex}
\usepackage{pst-all}
%\input{format.sty}
\usepackage[frenchb]{babel}
\usepackage[a4paper]{geometry}
\input{symboles.sty}


\geometry{hmargin=1cm, vmargin=1.5cm }


\newcommand{\JFC}[1]{\begin{color}{green}\textit{#1}\end{color}}

%
%\lstset{% general command to set parameter(s)
%basicstyle=\small,          % print whole listing small
%keywordstyle=\color{black}\bfseries\underbar,
                                % underlined bold black keywords
%identifierstyle=,           % nothing happens
%commentstyle=\color{white}, % white comments
%stringstyle=\ttfamily,      % typewriter type for strings
%extendedchars = true,
%showstringspaces=false}     % no special string spaces



\usepackage{hyperref}
\pdfcompresslevel=9
\hypersetup{
     %backref=true,    %permet d'ajouter des liens dans...
     %pagebackref=true,%...les bibliographies
     %hyperindex=true, %ajoute des liens dans les index.
     colorlinks=true, %colorise les liens
     breaklinks=true, %permet le retour à la ligne dans les liens trop longs
     urlcolor= blue, %couleur des hyperliens
     linkcolor= blue, %couleur des liens internes
     %bookmarks=true, %créé des signets pour Acrobat
     bookmarksopen=true,            %si les signets Acrobat sont créés,
                                    %les afficher complÚtement.
     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.
}




\makeindex

\newcommand{\inputladot}[2]{
\input{#1.dot.tex}
\includegraphics[width=#2]{#1.dot.ps}
}

\setcounter{secnumdepth}{4}

\renewcommand{\thesection}{\Roman{section}}
%\renewcommand{\thesubsection}{~~~~\arabic{subsection}}
%\renewcommand{\theparagraph}{~~~~~~~~\arabic{paragraph}}

\begin{document}


\title{Mémoire de synthèse des activités de recherche et d'encadrement.}
\author{Jean-Fran\c{c}ois {\sc Couchot}}


%\lstset{language=C}
\maketitle

\section{Curriculum vit{\ae} (1 page).}


\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}
\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 
\end{itemize}

\subsection{Diplômes universitaires}
\begin{itemize}
\item{\bf{91~:}} Baccalauréat série C mention AB, Besançon.
\item{\bf{95~:}} Maîtrise de mathématiques pures, Université de
  Franche-Comté (UFC).
\item{\bf{96~:}} 
CAPES de mathématiques, IUFM d'Auvergne.
\item{\bf{02~:}} 
Maîtrise d'informatique, mention B (UFC). 
\item{\bf{02~:}}
 DEA Informatique, option {\em Génie Logiciel} (UFC). Stage intitulé {\em Atteignabilité d'états et spécifications
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), 
sur la {\em vérification d'invariants par superposition}, 
mention très honorable.
\end{itemize}


\subsection{Fonctions et expériences professionnelles}
\begin{itemize}
\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
  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. 
 \end{itemize}


\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 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é 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}


\newpage
\section{Perspectives de recherche (1 à 2 pages maximum)}

\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…) ;

\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  ;

\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 ;


\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) ;
\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.

\section{Avis du directeur de l'Equipe}\label{sec:avis:directeur}

\bibliographystyle{alpha}
\bibliography{abbrev,biblioand}



\end{document}