From: Jean-François Couchot <couchot@couchot.iut-bm.univ-fcomte.fr>
Date: Mon, 17 Aug 2015 09:38:33 +0000 (+0200)
Subject: ajout syhthèse thèse
X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/commitdiff_plain/c9035994deb49df7f4452f1f4737481b1caf4b17

ajout syhthèse thèse
---

diff --git a/demandeInscription/synthese.tex b/demandeInscription/synthese.tex
index a9ba499..a2761f2 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,21 +140,163 @@ 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*{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)}
@@ -195,6 +337,9 @@ 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}