Durant mon travail de thèse intitulée
{\em vérification d'invariants par superposition},
-j'ai proposé différentes traductions en logique équationnelle
+j'ai proposé différentes traductions en logique équationnelle\cite{cdgr03:ij,cddg+04:ip,cg04:np}
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.
-
-
+J'ai appliqué ceci à la vérification de protocoles notamment d'exclusion
+mutuelle~\cite{CGK05} définies à l'aide de spécification ensemblises B~\cite{cdgr04:onp}.
\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.
\newpage
\section{Exposé des recherches réalisées au cours de la période postdoctorale}
-\JFC{chapeau à refaire}
+Entre avril 2006 et aujourdh'ui, les recherches réalisées ont concerné plusieursdomaines synthétisés ci-après. Le premier travail (Sec.~\ref{sub:verif})
+est une suite directe des travaux de thèse. Suivent six sections
+(de la Sec.~\ref{sub:sdd} à la Sec.~\ref{sub:ih}) sur les systèmes
+dynamiques discrets et leurs applications, thématique
+sur laquelle j'ai été recruté pour travailler dans l'équipe AND du département
+DISC. Enfin la section~\ref{sub:gen} présente comment j'ai réinvesti le nouveau
+domaine de la bio-info à l'aide de compétences connexes.
+
-\subsection{Convergence de systèmes dynamiques discrets}
+\subsection{Vérification de programmes par
+ preuve automatique}\label{sub:verif}
+
+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{Convergence de systèmes dynamiques discrets}\label{sub:sdd}
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}.
+%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.
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})
+\emph{itérations mixes} (introduit par Pr. J. M. Bahi en2005 notamment)
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.
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}.
+Des méthodes de simulation basées sur des stratégies et des délais générés aléatoirement avaient déjà été présentées.
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.
\subsection{Construction de fonctions chaotiques}
-Pr. Christophe Guyeux de l'équipe AND a proposé dans sa thèse~\cite{guyeuxphd}
+Pr. Christophe Guyeux de l'équipe AND a proposé dans sa thèse en 2010
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
d'obtention d'une distribution uniforme d'un générateur construit en enlevant un chemin hamiltonien équilibré dans un $n$-cube. Le travail est en cours de soumission
en journal international.
+Enfin j'ai été sollicité pour encadrer une thèse sur l'implantation
+de générateurs de nombre pseudo-aléatoires à bases d'itérations
+chaotiques sur des circuits logiques
+programmables. J'ai commencé ce travail en encadrant une étude exhaustive
+de toutes les instances d'implantations de cette classe.
+Ce travail complet théorique et pratique est terminé aujourd'hui et
+est en cours de soumission dans un journal international.
+
+
+
-\subsection{Masquage d'information}
+
+\subsection{Masquage d'information}\label{sub:ih}
La propriété de transitivité des fonctions chaotiques implique que l'on peut
atteindre tout point depuis le voisinage de n'importe quel point.
-\subsection{Application à la génomique}
+\subsection{Application à la génomique}\label{sub:gen}
-Core génome
+Ayant acquis des compétences sur certaines structures de mathématiques
+discrètes (particulièrement théorie des graphe,
+relation d'équivalence,\ldots), j'ai pu contribuer en bio-informatique
+en les réappliquant notamment.
+Une de mes première piste de travail a été de proposer une méthode automatique
+de construction d'un ensemble de gènes communs (nommés core-génôm)
+à une famille de génômes.
+La méthode s'appuie sur la construction du graphe de similarité
+entre les gènes quotienté selon une relation d'équivalence pour en
+réduire sa taille. Chaque gènes est assimilé à son représentant de
+classe dans chaque génôme. Le core-genome se déduit comme l'intersection
+de tous les génôme. Ceci a donné lieu aux
+publications~\cite{acgs13:onp,akgcs+14:oip,acgm+14:ij}.
+
+L'approche précédente souffrait de n'engendrer que des core-génômes de (trop)
+petits cardinaux. J'ai contribué notamment
+à l'amélioration de la méthode en proposant une étape d'optimization issue
+d'une adaptation discrète la méthode d'essaims particulaires~\cite{aagp+15:ip}.
-\subsection*{Publications issues de ces recherches}
\newpage
\section{Perspectives de recherche (1 à 2 pages maximum)}
+\subsection{Les codes de Gray}
+
+L'utilisation des codes de Gray dans une démarche d'apprentissage
+(d'ecoulement d'air ou de fonctions chaotiques) ne s'est pas révélée comme
+concluante. Dans chacun des cas, la distance de Hamming entre deux
+configurations voisines peut etre très petite tandis que le chemin (dans le
+cycle hamitlonien) qui les relie peut être long et ce même
+pour des codes équilibrés.
+Je propose de travailler sur ce problème discret en mesurant la qualité
+du code de Gray à l'aide d'une fonction basée sur la longueur des chemins
+(du cycle hamiltonien) entre les configurations voisines.
+Je pense ainsi réduire ce problème à un problème d'optimisation et dégager
+une démarche de génération, comme je l'ai fait en bio-informatique.
+
+Jusqu'à présent, la production de codes de Gray équilibrés
+dans l'étape de construction de fonctions chaotiques pour la génération
+de nombres pseudo aléatoire bute sur des problèmes d'explosion combinatoire:
+les seuls algorithmes connus répondant à ce problème nécessitent a priori
+plus de $10^{36}$ évaluations pour $n=8$,
+ce qui n'est pas raisonnable de mettre en
+pratique lorsque chacune d'entre-elle prend 1s. On peut peut-être
+se contenter de code ``presque'' équilibrés, à défaut de pouvoir
+trouver ceux qui seront équilibrés.
+Je propose d'investiguer
+dans cette thématique en exploitant des approches itératives permettant
+d'optenir des optimums locaux et trouver ainsi des codes presque approximés.
+
+
+
+\subsection{Génération de nombres pseudo-alléatoires}
+
+La démarche actuelle de génération de nombres pseudo-alléatoires
+consiste à marcher dans une partie d'un $n$-cube en choisissant son chemin
+à l'aide d'un générateur fourni en entrée. Or ces générateurs sont tous des
+fonctions de $\{0,1\}^n$ dans lui même. Le problème semble pouvoir se réécrire
+comme un produit de deux automates à définir et à étudier.
+Je pense investiguer cette vois pour améliorer notre approche et
+s'affranchir, à terme, de tout autre générateur.
+Les propriété établies notament sur les temps d'arrêt devraient être conservées.
+il restera à le prouver.
+
+
+Jusqu'à présent, une seule expérimentation d'implantation de nos générateurs
+sur des dispositifs physiques comme les FPGAs a été réalisée. Celle-ci
+s'est faite automatiquement à l'aide de l'outil Matlab. Si le code engendré
+sur le circuit est bien une implantation fidèle à la spécification,
+il n'en est pas pour le autant efficace: le nombre de bits généré par surface
+est plutôt faible. Nous allons exploiter les meilleurs démarches mises en
+exherbe lors de la rédaction d'un état de l'art exhaustif sur les PRNG
+implantés sur FPGA pour produire du code optimisé.
+Je prévois de réaliser ceci dans la thèse de M. BAKIRI, en cours.
+
+Pour générér une fonction dont la matrice de Markov est doublement
+stochastique, nous avons proposé principalement deux méthodes
+(génération puis test, suppresion de chemin hamiltonien dans un $n$-cube).
+Ces deux méthodes ne passent pas à l'échelle, même pour des $n$ de ptite taille.
+Je pense attaquer ce problème algébriquement et en programmation logique avec
+contraintes. Dans le premier cas, on peut remarque composée de $1$ uniquement
+en $(i,i+1)$ est une réponse trivale au problème. Elle n'entre cependant dans
+aucune des solutions des deux premières démarches. Je pense continuer l'étude
+de ce genre de matrices et proposer une méthode plus générale de génération.
+Je prévois de réaliser ce travail avec M. S. Contassot, Pr à l'Université de Loraine.
+Le département DISC et l'équipe VESONTION
+a de fortes compétences en programmation logique avec
+contraintes. J'ai déjà démontré que ce problème peut être solluble par cette
+approche, sans avoir pour autant réussi à le faire.
+Je prévois des collaborations avec l'équipe VESONTIO du DISC sur ce sujet.
+
+
+Enfin, marcher dans une partie d'un $n$-cube est le modèle théorique que
+nous avons établi pour notre classe de générateur. On pourrait cependant
+penser à ``sauter'' dans ce $n$-cube, c'est à dire modifier plusieurs bits
+en une seule itération. J'ai commencé à étudier ce modèle avec les résultats
+pratiques suivants: le nombre d'itérations suffisant pour un mélange
+correct est plus petit que celui obtenu en marchant. De plus,
+il diminue à mesure que $n$ augmente ce qui n'est pas le cas en marchant.
+Cependant, pour l'instant, nous n'avons pas réussi à obtenir des bornes
+du temps d'arrêt. Je propose d'investiguer aussi dans cette direction.
+
+
+
+\subsection{Masquage d'information}
+Jusqu'à présent, autant que je sache les méthodes algébriques
+de réducution de domaine (analyse par composant principaux, SVD)
+n'ont pas été intégrées dans les outils permettant de décider si un
+média contient ou non un message caché. Ces méthodes ont déjà été
+appliquées avec succès lorsqu'elles sont combinées avec des méthodes
+d'apprentissage, par exemple dans de la reconnaissance faciale.
+
+
+
+\subsection{Bio-informatique}
+
+reconstruction d'ancètre
+
+
+
+
+
+
\newpage
\section{Insertion dans l'équipe de recherche (3 pages maximum).}
Rôle personnel joué dans l'animation de la recherche au
