[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*{Publication 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)}

(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{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{biblio}
\include{Bibliographie}


\end{document}