Difference between revisions of "Enseignant-chercheur, équipe automates et vérification"

From LRDE

 
Line 1: Line 1:
L'[http://epita.fr EPITA] est une école d'ingénieur (CTI), reconnue comme une école majeure dans le domaine de l'informatique. Elle fait partie du [https://www.usinenouvelle.com/comparatif-des-ecoles-d-ingenieurs-2018 classement 2018 de l'Usine Nouvelle] qui lui a attribué la 12e place au classement général des grandes écoles. Son statut d'établissement privé lui permet une grande réactivité et liberté d'action.
+
L'[http://epita.fr EPITA] est une école d'ingénieurs (CTI), reconnue comme une école majeure dans le domaine de l'informatique. Elle fait partie du [https://www.usinenouvelle.com/comparatif-des-ecoles-d-ingenieurs-2018 classement 2018 de l'Usine Nouvelle] qui lui a attribué la 12e place au classement général des grandes écoles. Son statut d'établissement privé lui permet une grande réactivité et liberté d'action.
   
L'activité de recherche à l'EPITA s'appuie en premier lieu sur le [https://www.lrde.epita.fr Laboratoire de Recherche et Développement de l'EPITA (LRDE)]. Créé en 1998, il comprend aujourd'hui une trentaine de membres : enseignants-chercheurs, un support administratif, des doctorants et quelques élèves de l'école sélectionnés pour travailler avec les permanents. Il dispose d'une large autonomie vis-à-vis de l'EPITA. Les thématiques du LRDE sont le traitement d'images (de la morphologie mathématique aux réseaux neuronaux) et la théorie des automates avec un accent sur le ''model-checking''. Le LRDE est membre de l'école doctorale EDITE de Paris, et a été évalué par le Hcéres en 2018. Son rapport d'activité ainsi que ses publications sont disponibles [https://www.lrde.epita.fr/wiki/Publications ici].
+
L'activité de recherche à l'EPITA s'appuie en premier lieu sur le [https://www.lrde.epita.fr Laboratoire de Recherche et Développement de l'EPITA (LRDE)]. Créé en 1998, il comprend aujourd'hui une trentaine de membres : enseignants-chercheurs, un support administratif, des doctorants et quelques élèves de l'école sélectionnés pour travailler avec les permanents. Il dispose d'une large autonomie vis-à-vis de l'EPITA. Les thématiques du LRDE sont le traitement d'images (de la morphologie mathématique aux réseaux neuronaux) et la théorie des automates avec un accent sur le ''model-checking''. Le LRDE est membre de l'école doctorale [http://edite-de-paris.fr/ EDITE de Paris], et a été évalué par le Hcéres en 2018 ([https://www.hceres.fr/content/download/32481/495721/file/D2019-EV-0942095S-DER-PUR190016582-023142-RF.pdf PDF]). Son rapport d'activité ainsi que ses publications sont disponibles [https://www.lrde.epita.fr/wiki/Publications ici].
   
 
==== Recherche ====
 
==== Recherche ====

Latest revision as of 09:51, 28 November 2018

L'EPITA est une école d'ingénieurs (CTI), reconnue comme une école majeure dans le domaine de l'informatique. Elle fait partie du classement 2018 de l'Usine Nouvelle qui lui a attribué la 12e place au classement général des grandes écoles. Son statut d'établissement privé lui permet une grande réactivité et liberté d'action.

L'activité de recherche à l'EPITA s'appuie en premier lieu sur le Laboratoire de Recherche et Développement de l'EPITA (LRDE). Créé en 1998, il comprend aujourd'hui une trentaine de membres : enseignants-chercheurs, un support administratif, des doctorants et quelques élèves de l'école sélectionnés pour travailler avec les permanents. Il dispose d'une large autonomie vis-à-vis de l'EPITA. Les thématiques du LRDE sont le traitement d'images (de la morphologie mathématique aux réseaux neuronaux) et la théorie des automates avec un accent sur le model-checking. Le LRDE est membre de l'école doctorale EDITE de Paris, et a été évalué par le Hcéres en 2018 (PDF). Son rapport d'activité ainsi que ses publications sont disponibles ici.

Recherche

Le LRDE recrute un ou une Maître de Conférences afin de renforcer l'équipe Automates et Vérification. Constituée actuellement de deux enseignants-chercheurs (un professeur et un maître de conférence), son activité s'articule autour de la plate-forme Spot, une bibliothèque (écrite en C++) de manipulation de formules LTL (et du fragment linéaire de PSL) et d'automates sur les mots infinis (ω-automates). Le profil recherché s'intègre dans cette thématique. Les points forts de Spot sont aujourd'hui:

  • la traduction de formules LTL/PSL vers des ω-automates (avec diverses conditions d'acceptation) ;
  • la manipulation d'ω-automates: simplification, déterminisation, changement de conditions d'acceptation... ;
  • le model-checking, essentiellement via des opérations de produits d'automates et des tests de vacuité ;
  • plus récemment, l'utilisation d'ω-automates pour des problèmes de synthèse et la résolution de jeux à parité.

Le profil idéal associe un intérêt marqué pour la théorie des automates en lien avec la vérification formelle à de solides compétences de programmation lui permettant de participer activement au développement de Spot. Le projet de recherche pourra proposer des axes de développement, aussi bien en termes de nouvelles fonctionnalités que d'intégration avec d'autres outils/systèmes de vérification ou de renforcement et optimisation de fonctionnalités existantes.

Enseignement

La personne recrutée sera appelée à intervenir et à prendre la responsabilité de différents cours dans tous les niveaux du cursus ingénieur (Bac+3 à Bac+5) de l'EPITA. Pour cette raison, une expérience d'enseignement sera appréciée.

Procédure de recrutement

Envoyez un CV (incluant une liste de publications), une lettre de motivation ainsi qu'un court document (1 à 2 pages) résumant votre projet de recherche à info@lrde.epita.fr . Les candidats retenus seront invités à venir présenter leurs travaux et leur projet aux membres du laboratoire. Le projet de recherche pourra être discuté et affiné au cours de ces discussions.

Pour toute question ou renseignement, les candidats potentiels sont invités à prendre contact avec les membres de l'équipe qui seront heureux de dissiper leurs interrogations.