Marc ZEITOUN
Marc Zeitoun Professeur (Université Bordeaux 1)

Équipe LaBRI : Méthodes formelles
Fonction administrative : Directeur adjoint. Responsable de la Licence Informatique.
Page personnelle : http://www.labri.fr/~zeitoun
Courrier électronique : marc.zeitounarobaselabri.fr
Bureau : 202
Tél : +33 (0)5 40 00 60 94


Recherche

Mon travail de recherche en informatique s'inscrit dans le cadre des méthodes formelles, avec comme objectif principal la
vérification de logiciel. Cette problématique, datant déjà de plusieurs années, s'affirme aujourd'hui comme l'un des défis majeurs.
Les dispositifs informatiques, hier confinés à des applications spécialisées, sont omniprésents (commerce électronique, systèmes
embarqués, contrôle des réseaux de transport, médecine, énergie, finance, etc.), et des erreurs logicielles peuvent entraîner des
coûts humains ou économiques considérables. Il est donc crucial de pouvoir détecter ces erreurs afin d'acquérir une confiance
maximale dans les logiciels critiques. Les méthodes formelles fournissent un cadre rigoureux pour attaquer le problème de
vérification.

Une partie de mes travaux porte sur la vérification d'applications distribuées. Je m'intéresse en particulier au problème de
synthèse de contrôleur. Bien maîtrisé dans le cadre séquentiel, ce problème est nettement moins bien compris dans le cadre
distribué, où plusieurs entités communiquent pour réaliser un système global. Je collabore sur cette thématique avec Paul Gastin
(LSV, ENS Cachan), avec qui nous avons déjà obtenu des résultats de décidabilité marquants.

Un autre axe dans lequel je m'investis consiste à développer des outils algébriques et topologiques pour répondre à des questions
algorithmiques. J'entretiens depuis plusieurs années une collaboration avec J. Almeida (U. Porto, Portugal) et J.C. Costa (U. Minho,
Portugal) ayant donné lieu à plusieurs publications communes. Ce cadre reste relié à des problématiques de vérification, d'un
point de vue plus théorique. Nous avons récemment obtenu un algorithme alternatif à un problème difficile de séparation, ou
interpolation, qui intervient naturellement dans d'autres domaines.

Enfin, depuis récemment, je m'intéresse à la vérification de certains systèmes infinis. Je développe actuellement cette thématique
dans le cadre de la délégation dont je bénéficie pour l'année 2009-2010 au LSV, Laboratoire Spécification et Vérification de l'ENS
Cachan. Je m'intéresse en particulier à des problèmes quantitatifs, concernant le contrôle de la quantité de ressources qu'un
système peut ou doit utiliser. Des résultats préliminaires ont été obtenus lors du stage d'un étudiant de l'IIT Bombay (mai-juillet
2009).

Extrait de publications













Responsabilité pédagogique

\begin{itemize}
\item Responsabilité du master recherche informatique Bordeaux 1, 2006-2009.

\item Responsable de plusieurs UE en licence et master, dont
\begin{itemize}
\item Création de cours Master 2 "Algorithmes pour le monde réel" avec C. Gavoille et A. Muscholl.
\item Responsable de l'UE "Initiation à la recherche", Master, semestre 3, 2006-2009.
\item Rénovation de l'UE "Initiation à l'informatique", Licence, semestre 1, 2005-2008.
\end{itemize}
\end{itemize}

Administration

\begin{itemize}
\item Responsable du master recherche, département informatique, UFR MI Bordeaux 1 2006–2009.
\item Membre de la commission de spécialistes Bordeaux 1 2006–2008.
\item Membre de 3 comités de sélection en 2008-2009 (PR ENSEIRB, MCF Paris 7 et PR Paris 7).
\item Membre nommé du conseil de laboratoire du LaBRI 2007–2009.
\item Membre du conseil de l'école doctorale MI Bordeaux 1 2007–2009.
\item Mise en place et maintenance du site web de STACS, \url{http://stacs-conf.org} depuis 2007.
\end{itemize}


Page mise à jour le 13/08/2010 à 10:56