From c9035994deb49df7f4452f1f4737481b1caf4b17 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Jean-Fran=C3=A7ois=20Couchot?= Date: Mon, 17 Aug 2015 11:38:33 +0200 Subject: [PATCH] =?utf8?q?ajout=20syhth=C3=A8se=20th=C3=A8se?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit --- demandeInscription/synthese.tex | 159 ++++++++++++++++++++++++++++++-- 1 file changed, 152 insertions(+), 7 deletions(-) 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} -- 2.39.5