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